reconsider IT = addLoopStr(# the carrier of M, the addF of M,(0. M) #) as non empty addLoopStr ;
A1: for x, y, z being Element of IT holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )

proof

let x, y, z be Element of IT; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
reconsider x9 = x, y9 = y, z9 = z as Element of M ;
thus x + y = y9 + x9 by RLVECT_1:2
.= y + x ; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def 3
.= x + (y + z) ; :: thesis: ( x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
thus x + (0. IT) = x9 + (0. M)
.= x by RLVECT_1:4 ; :: thesis: ex v being Element of IT st x + v = 0. IT
consider b being Element of M such that
A2: x9 + b = 0. M by ALGSTR_0:def 11;
reconsider b9 = b as Element of IT ;
take b9 ; :: thesis: x + b9 = 0. IT
thus x + b9 = 0. IT by A2; :: thesis: verum

end;

IT is right_complementable

proof

let x be Element of IT; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x9 = x as Element of M ;
consider b being Element of M such that
A3: x9 + b = 0. M by ALGSTR_0:def 11;
reconsider b9 = b as Element of IT ;
take b9 ; :: according to ALGSTR_0:def 11 :: thesis: x + b9 = 0. IT
thus x + b9 = 0. IT by A3; :: thesis: verum

end;

hence addLoopStr(# the carrier of M, the addF of M,(0. M) #) is strict AbGroup by A1, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum