(f : Homomorphism C (ProdAlgebra I A)) (i:I) : Homomorphism C (A i) := hom_compose (hom_proj_prod_algebra I A i) f.
Require Import Import algebra_notations ne_list.notations. Import prod_algebra_notations.