theorem :: VECTSP_2:20

for SF being Skew-Field
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 )