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