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