theorem :: GROUP_1A:44

for A being Abelian addGroup holds
( addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is Abelian & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is add-associative & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_zeroed & addLoopStr(# the carrier of A, the addF of A,(0_ A) #) is right_complementable )