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
proof
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 )
proof
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;
hence y in rng i by FUNCT_1:def 3; :: thesis: verum
end;
rng i c= the carrier of G by RELAT_1:def 19;
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