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 A1, Lm3;
thus (comp (opp K)) . x = - z by VECTSP_1:def 13
.= (comp K) . x by A3, VECTSP_1:def 13 ; :: 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 A2, FUNCT_1:2; :: 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