let K be non empty strict doubleLoopStr ; :: thesis: for W being non empty RightModStr of 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 of 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:54;
A2: opp the lmult of (opp W) = opp (opp the rmult of W) by Th13
.= the rmult of W by FUNCT_4:54 ;
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 Th9
.= addLoopStr(# the carrier of W,the addF of W,the ZeroF of W #) by Th12 ;
hence opp (opp W) = RightModStr(# the carrier of W,the addF of W,the ZeroF of W,the rmult of W #) by A2, A1, Th10; :: thesis: verum