let A be commutative Group; :: thesis: ( addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is Abelian & addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is right_complementable )
set G = addLoopStr(# the carrier of A,the multF of A,(1_ A) #);
thus addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is Abelian :: thesis: ( addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is add-associative & addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is right_complementable )

proof

let a, b be Element of ; :: according to RLVECT_1:def 5 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of ;
A1: for a, b being Element of
for x, y being Element of st a = x & b = y holds
a + b = x * y ;
thus a + b = x * y
.= b + a by A1 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is right_zeroed & addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is right_complementable )

let a, b, c be Element of ; :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of ;
thus (a + b) + c = (x * y) * z
.= x * (y * z) by Def4
.= a + (b + c) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: addLoopStr(# the carrier of A,the multF of A,(1_ A) #) is right_complementable

let a be Element of ; :: thesis: a + (0. addLoopStr(# the carrier of A,the multF of A,(1_ A) #)) = a
reconsider x = a as Element of ;
thus a + (0. addLoopStr(# the carrier of A,the multF of A,(1_ A) #)) = x * (1_ A)
.= a by Def5 ; :: thesis: verum

end;

let a be Element of ; :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Element of ;
reconsider b = (inverse_op A) . x as Element of ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. addLoopStr(# the carrier of A,the multF of A,(1_ A) #)
thus a + b = x * (x " ) by Def7
.= 0. addLoopStr(# the carrier of A,the multF of A,(1_ A) #) by Def6 ; :: thesis: verum