let K be non empty doubleLoopStr ; :: thesis: for V being non empty VectSpStr of K holds the rmult of (opp V) = opp the lmult of V
let V be non empty VectSpStr of K; :: thesis: the rmult of (opp V) = opp the lmult of V
reconsider p = ~ the lmult of V as Function of [:the carrier of V,the carrier of (opp K):],the carrier of V ;
opp V = RightModStr(# the carrier of V,the addF of V,(0. V),p #) by Def2;
hence the rmult of (opp V) = opp the lmult of V ; :: thesis: verum