let G1 be Group; :: thesis: for f being Function of the carrier of G1, the carrier of (product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is Homomorphism of G1,(product <*G1*>)
let f be Function of the carrier of G1, the carrier of (product <*G1*>); :: thesis: ( ( for x being Element of G1 holds f . x = <*x*> ) implies f is Homomorphism of G1,(product <*G1*>) )
assume A1: for x being Element of G1 holds f . x = <*x*> ; :: thesis: f is Homomorphism of G1,(product <*G1*>)

now :: thesis: for a, b being Element of G1 holds f . (a * b) = (f . a) * (f . b)

let a, b be Element of G1; :: thesis: f . (a * b) = (f . a) * (f . b)
thus f . (a * b) = <*(a * b)*> by A1
.= <*a*> * <*b*> by Th28
.= <*a*> * (f . b) by A1
.= (f . a) * (f . b) by A1 ; :: thesis: verum

end;

hence f is Homomorphism of G1,(product <*G1*>) by GROUP_6:def 6; :: thesis: verum