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 U2 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 U2 of W,the rmult of W #)
set V = opp W;
A1: addLoopStr(# the carrier of (opp (opp W)),the addF of (opp (opp W)),the U2 of (opp (opp W)) #) = addLoopStr(# the carrier of (opp W),the addF of (opp W),the U2 of (opp W) #) by Th9
.= addLoopStr(# the carrier of W,the addF of W,the U2 of W #) by Th12 ;
A2: opp the lmult of (opp W) = opp (opp the rmult of W) by Th13
.= the rmult of W by FUNCT_4:54 ;
opp (opp K) = K by FUNCT_4:54;
hence opp (opp W) = RightModStr(# the carrier of W,the addF of W,the U2 of W,the rmult of W #) by A1, A2, Th10; :: thesis: verum