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

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