theorem Th9: :: MOD_4:9

for K being non empty doubleLoopStr
for W being non empty RightModStr over K holds
( addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) = addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) & ( for x being set holds
( x is Vector of W iff x is Vector of (opp W) ) ) )