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