let G be non empty well-unital multLoopStr ; :: thesis: ex h being Homomorphism of G,G st h is bijective

reconsider i = id the carrier of G as Homomorphism of G,G by Th13;

A1: the carrier of G c= rng i

then rng i = the carrier of G by A1, XBOOLE_0:def 10;

then i is onto ;

hence ex h being Homomorphism of G,G st h is bijective ; :: thesis: verum

reconsider i = id the carrier of G as Homomorphism of G,G by Th13;

A1: the carrier of G c= rng i

proof

rng i c= the carrier of G
by RELAT_1:def 19;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of G or y in rng i )

assume A2: y in the carrier of G ; :: thesis: y in rng i

ex x being set st

( x in dom i & y = i . x )

end;assume A2: y in the carrier of G ; :: thesis: y in rng i

ex x being set st

( x in dom i & y = i . x )

proof

hence
y in rng i
by FUNCT_1:def 3; :: thesis: verum
take
y
; :: thesis: ( y is set & y in dom i & y = i . y )

thus ( y is set & y in dom i & y = i . y ) by A2, FUNCT_1:17; :: thesis: verum

end;thus ( y is set & y in dom i & y = i . y ) by A2, FUNCT_1:17; :: thesis: verum

then rng i = the carrier of G by A1, XBOOLE_0:def 10;

then i is onto ;

hence ex h being Homomorphism of G,G st h is bijective ; :: thesis: verum