theorem Th7: :: MOD_4:7

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