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 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 holds f . x = <*x*> ) implies f is Homomorphism of G1, product <*G1*> )
assume A1: for x being Element of holds f . x = <*x*> ; :: thesis: f is Homomorphism of G1, product <*G1*>

now

let a, b be Element of ; :: thesis: f . (a * b) = (f . a) * (f . b)
thus f . (a * b) = <*(a * b)*> by A1
.= <*a*> * <*b*> by Th31
.= <*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 7; :: thesis: verum