let G be non empty right_unital left_unital associative multLoopStr ; :: thesis: ( G is Group-like implies units G = the carrier of G )
assume A1: G is Group-like ; :: thesis: units G = the carrier of G
for x being object st x in the carrier of G holds
x in units G

proof

let x be object ; :: thesis: ( x in the carrier of G implies x in units G )
assume x in the carrier of G ; :: thesis: x in units G
then reconsider g = x as Element of G ;
consider e being Element of G such that
A2: for h being Element of G holds
( h * e = h & e * h = h & ex g9 being Element of G st
( h * g9 = e & g9 * h = e ) ) by A1, GROUP_1:def 2;
1. G = (1. G) * e by A2
.= e ;
then ex y being Element of G st
( g * y = 1. G & y * g = 1. G ) by A2;
then g is unital by GCD_1:def 2;
hence x in units G ; :: thesis: verum

end;

then the carrier of G c= units G by TARSKI:def 3;
hence units G = the carrier of G by XBOOLE_0:def 10; :: thesis: verum