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*>)

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

f is one-to-one
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, FINSEQ_1:def 8;

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;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, FINSEQ_1:def 8;

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

proof

hence
f is bijective
by A3, GROUP_6:60; :: thesis: verum
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;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