for G1 being Group
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*>)