theorem :: VECTSP_2:22

for SF being Skew-Field
for x, y being Scalar of SF st y <> 0. SF holds
(x / y) * y = x