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 ) ) )

thus ( x is Scalar of (opp K) iff x is Scalar of K ) ; :: thesis: verum

( 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 )

let x be set ; :: thesis: ( x is Scalar of (opp K) iff x is Scalar of K )( 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

hence comp (opp K) = comp K by A2, FUNCT_1:2; :: thesis: verum

end;A2: for x being object st x in the carrier of K holds

(comp (opp K)) . x = (comp K) . x

proof

( dom (comp (opp K)) = the carrier of K & dom (comp K) = the carrier of K )
by FUNCT_2:def 1;
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;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

hence comp (opp K) = comp K by A2, FUNCT_1:2; :: thesis: verum

thus ( x is Scalar of (opp K) iff x is Scalar of K ) ; :: thesis: verum