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