let K be non empty doubleLoopStr ; :: thesis: for W being non empty RightModStr over K holds the lmult of (opp W) = opp the rmult of W
let W be non empty RightModStr over 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 = ModuleStr(# 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