theorem Th38: :: GROUP_7:38
for G1 being Group
for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is bijective