let SF be Skew-Field; :: thesis: for x, y, z being Scalar of SF st z <> 0. SF holds
( (x / z) + (y / z) = (x + y) / z & (x / z) - (y / z) = (x - y) / z )
let x, y, z be Scalar of SF; :: thesis: ( z <> 0. SF implies ( (x / z) + (y / z) = (x + y) / z & (x / z) - (y / z) = (x - y) / z ) )
( z <> 0. SF implies (x / z) - (y / z) = (x - y) / z )

proof

assume z <> 0. SF ; :: thesis: (x / z) - (y / z) = (x - y) / z
hence (x / z) - (y / z) = (x / z) + ((- y) / z) by Th19
.= (x - y) / z by VECTSP_1:def 7 ;
:: thesis: verum

end;

hence ( z <> 0. SF implies ( (x / z) + (y / z) = (x + y) / z & (x / z) - (y / z) = (x - y) / z ) ) by VECTSP_1:def 7; :: thesis: verum