let SF be Skew-Field; :: thesis: for x, y being Scalar of SF st y <> 0. SF holds
( - (x / y) = (- x) / y & x / (- y) = - (x / y) )
let x, y be Scalar of SF; :: thesis: ( y <> 0. SF implies ( - (x / y) = (- x) / y & x / (- y) = - (x / y) ) )
assume y <> 0. SF ; :: thesis: ( - (x / y) = (- x) / y & x / (- y) = - (x / y) )
then A1: - y <> 0. SF by Th3;
thus A2: - (x / y) = (- x) / y by VECTSP_1:9; :: thesis: x / (- y) = - (x / y)
- (1. SF) <> 0. SF by Th3;
then x / (- y) = (x * (- (1_ SF))) / ((- y) * (- (1_ SF))) by A1, Th18;
then x / (- y) = (- (x * (1_ SF))) / ((- y) * (- (1_ SF))) by VECTSP_1:8
.= (- x) / ((- y) * (- (1_ SF)))
.= (- x) / (- ((- y) * (1_ SF))) by VECTSP_1:8
.= (- x) / ((- (- y)) * (1_ SF))
.= (- x) / (y * (1_ SF)) by RLVECT_1:17
.= - (x / y) by A2 ;
hence x / (- y) = - (x / y) ; :: thesis: verum