reconsider IT = addLoopStr(# the carrier of R,the addF of R,(0. R) #) as non empty addLoopStr ;
A1: IT is right_complementable

proof

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

end;

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 x' = x, y' = y, z' = z as Scalar of R ;
thus x + y = y' + x' by RLVECT_1:5
.= 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 = (x' + y') + z'
.= x' + (y' + z') by RLVECT_1:def 6
.= x + (y + z) ; :: thesis: ( x + (0. IT) = x & ex v being Element of IT st x + v = 0. IT )
thus x + (0. IT) = x' + (0. R)
.= x by RLVECT_1:10 ; :: thesis: ex v being Element of IT st x + v = 0. IT
consider b being Scalar of R such that
A3: x' + b = 0. R by ALGSTR_0:def 11;
reconsider b' = b as Element of IT ;
take b' ; :: thesis: x + b' = 0. IT
thus x + b' = 0. IT by A3; :: thesis: verum

end;

hence addLoopStr(# the carrier of R,the addF of R,(0. R) #) is strict AbGroup by A1, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7; :: thesis: verum