for K being non empty strict doubleLoopStr
for V being non empty ModuleStr over K holds opp (opp V) = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)