deffunc H₁( Element of I) -> Element of bool [: the carrier of (product F1), the carrier of (F2 . $1):] = (f . $1) * (proj (F1,$1));
A1: for i being Element of I holds H₁(i) is Homomorphism of (product F1),(F2 . i) ;
consider phi being Homomorphism-Family of product F1,F2 such that
A2: for i being Element of I holds phi . i = H₁(i) from GROUP_23:sch 5(A1);
take psi = product phi; :: thesis: for i being Element of I holds (proj (F2,i)) * psi = (f . i) * (proj (F1,i))
thus for i being Element of I holds (proj (F2,i)) * psi = (f . i) * (proj (F1,i)) :: thesis: verum

proof

let i be Element of I; :: thesis: (proj (F2,i)) * psi = (f . i) * (proj (F1,i))
for g being Element of (product F1) holds ((proj (F2,i)) * psi) . g = ((f . i) * (proj (F1,i))) . g

proof

let g be Element of (product F1); :: thesis: ((proj (F2,i)) * psi) . g = ((f . i) * (proj (F1,i))) . g
B1: dom psi = the carrier of (product F1) by FUNCT_2:def 1;
H₁(i) . g = (phi . i) . g by A2
.= (psi . g) . i by Def14
.= (proj (F2,i)) . (psi . g) by Def13
.= ((proj (F2,i)) * psi) . g by B1, FUNCT_1:13 ;
hence ((proj (F2,i)) * psi) . g = ((f . i) * (proj (F1,i))) . g ; :: thesis: verum

end;

hence (proj (F2,i)) * psi = (f . i) * (proj (F1,i)) by FUNCT_2:def 8; :: thesis: verum

end;