let K be non empty doubleLoopStr ; :: thesis: for V being non empty ModuleStr over K holds the rmult of (opp V) = opp the lmult of V

let V be non empty ModuleStr over 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

let V be non empty ModuleStr over 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