let K be Skew-Field; :: thesis: opp K is Skew-Field
set L = opp K;
for x being Scalar of (opp K) holds
( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )

proof

let x be Scalar of (opp K); :: thesis: ( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )
( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) )

proof

reconsider a = x as Scalar of K ;
assume x <> 0. (opp K) ; :: thesis: ex y being Scalar of (opp K) st y * x = 1_ (opp K)
then consider b being Scalar of K such that
A1: a * b = 1_ K by VECTSP_2:6;
reconsider y = b as Scalar of (opp K) ;
take y ; :: thesis: y * x = 1_ (opp K)
thus y * x = 1_ (opp K) by A1, Lm3; :: thesis: verum

end;

hence ( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) ) ; :: thesis: verum

end;

hence opp K is Skew-Field by STRUCT_0:def 8, VECTSP_1:def 9; :: thesis: verum