let K be non empty doubleLoopStr ; :: thesis: 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) ) ) )
let W be non empty RightModStr over K; :: thesis: ( 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) ) ) )
reconsider p = ~ the rmult of W as Function of [: the carrier of (opp K), the carrier of W:], the carrier of W ;
A1: opp W = ModuleStr(# the carrier of W, the addF of W,(0. W),p #) by Def4;
hence 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 #) ; :: thesis: for x being set holds
( x is Vector of W iff x is Vector of (opp W) )
let x be set ; :: thesis: ( x is Vector of W iff x is Vector of (opp W) )
thus ( x is Vector of W iff x is Vector of (opp W) ) by A1; :: thesis: verum