let K be non empty doubleLoopStr ; :: thesis: ( addLoopStr(# the carrier of (opp K), the addF of (opp K), the ZeroF of (opp K) #) = addLoopStr(# the carrier of K, the addF of K, the ZeroF of K #) & ( K is add-associative & K is right_zeroed & K is right_complementable implies comp (opp K) = comp K ) & ( for x being set holds
( x is Scalar of (opp K) iff x is Scalar of K ) ) )

thus addLoopStr(# the carrier of (opp K), the addF of (opp K), the ZeroF of (opp K) #) = addLoopStr(# the carrier of K, the addF of K, the ZeroF of K #) ; :: thesis: ( ( K is add-associative & K is right_zeroed & K is right_complementable implies comp (opp K) = comp K ) & ( for x being set holds
( x is Scalar of (opp K) iff x is Scalar of K ) ) )

hereby :: thesis: for x being set holds
( x is Scalar of (opp K) iff x is Scalar of K )
assume A1: ( K is add-associative & K is right_zeroed & K is right_complementable ) ; :: thesis: comp (opp K) = comp K
A2: for x being object st x in the carrier of K holds
(comp (opp K)) . x = (comp K) . x
proof
let x be object ; :: thesis: ( x in the carrier of K implies (comp (opp K)) . x = (comp K) . x )
assume x in the carrier of K ; :: thesis: (comp (opp K)) . x = (comp K) . x
then reconsider y = x as Element of K ;
reconsider z = y as Element of (opp K) ;
A3: - y = - z by ;
thus (comp (opp K)) . x = - z by VECTSP_1:def 13
.= (comp K) . x by ; :: thesis: verum
end;
( dom (comp (opp K)) = the carrier of K & dom (comp K) = the carrier of K ) by FUNCT_2:def 1;
hence comp (opp K) = comp K by ; :: thesis: verum
end;
let x be set ; :: thesis: ( x is Scalar of (opp K) iff x is Scalar of K )
thus ( x is Scalar of (opp K) iff x is Scalar of K ) ; :: thesis: verum