let M be non empty well-unital associative multLoopStr ; :: thesis: 1_ (UnitGroup M) = 1. M
1. M in the carrier of (UnitGroup M) ;
then reconsider e = 1. M as Element of (UnitGroup M) ;
for x being Element of (UnitGroup M) holds
( x * e = x & e * x = x )

proof

let x be Element of (UnitGroup M); :: thesis: ( x * e = x & e * x = x )
x in units M ;
then reconsider a = x as Element of M ;
thus x * e = a * (1. M) by Th110
.= x ; :: thesis: e * x = x
thus e * x = (1. M) * a by Th110
.= x ; :: thesis: verum

end;

hence 1_ (UnitGroup M) = 1. M by GROUP_1:4; :: thesis: verum