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