deffunc H₁() -> multMagma = product F;
deffunc H₂() -> multMagma = F . i;
deffunc H₃( Element of H₁()) -> Element of (F . i) = $1 /. i;
consider p being Function of H₁(),H₂() such that
A1: for x being Element of H₁() holds p . x = H₃(x) from FUNCT_2:sch 4();
reconsider p = p as Function of (product F),(F . i) ;
for a, b being Element of (product F) holds p . (a * b) = (p . a) * (p . b)

proof

let a, b be Element of (product F); :: thesis: p . (a * b) = (p . a) * (p . b)
(p . a) * (p . b) = (p . a) * (b /. i) by A1
.= (a /. i) * (b /. i) by A1
.= (a * b) /. i by GROUP_7:1
.= p . (a * b) by A1 ;
hence p . (a * b) = (p . a) * (p . b) ; :: thesis: verum

end;

then reconsider p = p as Homomorphism of (product F),(F . i) by GROUP_6:def 6;
take p ; :: thesis: for h being Element of (product F) holds p . h = h . i
for h being Element of (product F) holds p . h = h . i

proof

let h be Element of (product F); :: thesis: p . h = h . i
p . h = h /. i by A1;
hence p . h = h . i ; :: thesis: verum

end;

hence for h being Element of (product F) holds p . h = h . i ; :: thesis: verum