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 Th17;
rng i = the carrier of G

proof

thus rng i c= the carrier of G by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= rng i
thus the carrier of G c= rng i :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of G or y in rng i )
assume A1: y in the carrier of G ; :: thesis: y in rng i
ex x being set st
( x in dom i & y = i . x )

proof

take y ; :: thesis: ( y in dom i & y = i . y )
thus ( y in dom i & y = i . y ) by A1, FUNCT_1:34; :: thesis: verum

end;

hence y in rng i by FUNCT_1:def 5; :: thesis: verum

end;

end;

then ( i is one-to-one & i is onto ) by FUNCT_2:def 3;
then i is bijective ;
hence ex h being Homomorphism of G,G st h is bijective ; :: thesis: verum