let K be non empty doubleLoopStr ; :: thesis: for W being non empty RightModStr of K holds
( addLoopStr(# the carrier of (opp W),the addF of (opp W),the U2 of (opp W) #) = addLoopStr(# the carrier of W,the addF of W,the U2 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 of K; :: thesis: ( addLoopStr(# the carrier of (opp W),the addF of (opp W),the U2 of (opp W) #) = addLoopStr(# the carrier of W,the addF of W,the U2 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 = VectSpStr(# 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 U2 of (opp W) #) = addLoopStr(# the carrier of W,the addF of W,the U2 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