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 addLoopStr(# the carrier of A, the multF of A,(1_ A) #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of A ;
A1: for a, b being Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #)
for x, y being Element of A 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 3 :: 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 addLoopStr(# the carrier of A, the multF of A,(1_ A) #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of A ;
thus (a + b) + c = (x * y) * z
.= x * (y * z) by Def3
.= a + (b + c) ; :: thesis: verum

end;

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

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

end;

let a be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Element of A ;
reconsider b = (inverse_op A) . x as Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #) ;
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 Def6
.= 0. addLoopStr(# the carrier of A, the multF of A,(1_ A) #) by Def5 ; :: thesis: verum