let G1 be Group; :: thesis: for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is bijective
let f be Homomorphism of G1,(product <*G1*>); :: thesis: ( ( for x being Element of G1 holds f . x = <*x*> ) implies f is bijective )
assume A1: for x being Element of G1 holds f . x = <*x*> ; :: thesis: f is bijective
A2: dom f = the carrier of G1 by FUNCT_2:def 1;
A3: rng f = the carrier of (product <*G1*>)

proof

thus rng f c= the carrier of (product <*G1*>) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (product <*G1*>) c= rng f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (product <*G1*>) or x in rng f )
assume x in the carrier of (product <*G1*>) ; :: thesis: x in rng f
then reconsider a = x as Element of (product <*G1*>) ;
A4: 1 in {1} by TARSKI:def 1;
then A5: ex R being 1-sorted st
( R = <*G1*> . 1 & (Carrier <*G1*>) . 1 = the carrier of R ) by PRALG_1:def 15;
a in the carrier of (product <*G1*>) ;
then A6: a in product (Carrier <*G1*>) by Def2;
then A7: dom a = dom (Carrier <*G1*>) by CARD_3:9;
then A8: dom a = {1} by PARTFUN1:def 2;
then a . 1 in (Carrier <*G1*>) . 1 by A6, A7, A4, CARD_3:9;
then reconsider b = a . 1 as Element of G1 by A5;
f . b = <*b*> by A1
.= x by A8, FINSEQ_1:2, FINSEQ_1:def 8 ;
hence x in rng f by A2, FUNCT_1:def 3; :: thesis: verum

end;

f is one-to-one

proof

let m, n be object ; :: according to FUNCT_1:def 4 :: thesis: ( not m in dom f or not n in dom f or not f . m = f . n or m = n )
assume that
A9: m in dom f and
A10: n in dom f and
A11: f . m = f . n ; :: thesis: m = n
reconsider m1 = m, n1 = n as Element of G1 by A9, A10;
<*m1*> = f . m1 by A1
.= <*n1*> by A1, A11 ;
hence m = n by FINSEQ_1:76; :: thesis: verum

end;

hence f is bijective by A3, GROUP_6:60; :: thesis: verum