let G1 be Group; :: thesis: G1, product <*G1*> are_isomorphic

deffunc H_{1}( Element of G1) -> Element of (product <*G1*>) = <*$1*>;

consider f being Function of the carrier of G1, the carrier of (product <*G1*>) such that

A1: for x being Element of G1 holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

reconsider f = f as Homomorphism of G1,(product <*G1*>) by A1, Th37;

take f ; :: according to GROUP_6:def 11 :: thesis: f is bijective

thus f is bijective by A1, Th38; :: thesis: verum

deffunc H

consider f being Function of the carrier of G1, the carrier of (product <*G1*>) such that

A1: for x being Element of G1 holds f . x = H

reconsider f = f as Homomorphism of G1,(product <*G1*>) by A1, Th37;

take f ; :: according to GROUP_6:def 11 :: thesis: f is bijective

thus f is bijective by A1, Th38; :: thesis: verum