let G1 be Group; :: thesis: for f being Homomorphism of G1,() st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is bijective

let f be Homomorphism of 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 ()
proof
thus rng f c= the carrier of () ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of () c= rng f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of () or x in rng f )
assume x in the carrier of () ; :: thesis: x in rng f
then reconsider a = x as Element of () ;
A4: 1 in {1} by TARSKI:def 1;
then A5: ex R being 1-sorted st
( R = <*G1*> . 1 & () . 1 = the carrier of R ) by PRALG_1:def 15;
a in the carrier of () ;
then A6: a in product () by Def2;
then A7: dom a = dom () by CARD_3:9;
then A8: dom a = {1} by PARTFUN1:def 2;
then a . 1 in () . 1 by ;
then reconsider b = a . 1 as Element of G1 by ;
f . b = <*b*> by A1
.= x by ;
hence x in rng f by ; :: 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 ;
<*m1*> = f . m1 by A1
.= <*n1*> by ;
hence m = n by FINSEQ_1:76; :: thesis: verum
end;
hence f is bijective by ; :: thesis: verum