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*>)

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)

hence
f is Homomorphism of G1,(product <*G1*>)
by GROUP_6:def 6; :: thesis: verumlet 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;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