let K be non empty doubleLoopStr ; :: thesis: 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) ) ) )
let V be non empty ModuleStr over 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