theorem :: MOD_4:2

for K being non empty doubleLoopStr holds
( addLoopStr(# the carrier of (opp K), the addF of (opp K), the ZeroF of (opp K) #) = addLoopStr(# the carrier of K, the addF of K, the ZeroF of K #) & ( K is add-associative & K is right_zeroed & K is right_complementable implies comp (opp K) = comp K ) & ( for x being set holds
( x is Scalar of (opp K) iff x is Scalar of K ) ) )