let K be non empty strict doubleLoopStr ; :: thesis: for W being non empty RightModStr over K holds opp (opp W) = RightModStr(# the carrier of W, the addF of W, the ZeroF of W, the rmult of W #)
let W be non empty RightModStr over K; :: thesis: opp (opp W) = RightModStr(# the carrier of W, the addF of W, the ZeroF of W, the rmult of W #)
set V = opp W;
A1: opp (opp K) = K by FUNCT_4:53;
A2: opp the lmult of (opp W) = opp (opp the rmult of W) by Th10
.= the rmult of W by FUNCT_4:53 ;
addLoopStr(# the carrier of (opp (opp W)), the addF of (opp (opp W)), the ZeroF of (opp (opp W)) #) = addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) by Th7
.= addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) by Th9 ;
hence opp (opp W) = RightModStr(# the carrier of W, the addF of W, the ZeroF of W, the rmult of W #) by A2, A1, Th8; :: thesis: verum