(w : SymbolType σ) : (∀ i, Operation (A i) w) → Operation carriers_prod_algebra w := match w return (∀ i, Operation (A i) w) → Operation carriers_prod_algebra w with | [:_:] => idmap | _ ::: g => λ f p, g (λ i, f i (p i)) end.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.