let A be commutative Group; ( 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
( 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 )
let a be Element of addLoopStr(# the carrier of A, the multF of A,(1_ A) #); ALGSTR_0:def 16 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
; ALGSTR_0:def 11 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
; verum