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