let G1 be Group; :: thesis: G1, product <*G1*> are_isomorphic
deffunc H₁( 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₁(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