theorem :: VECTSP_2:17

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
x / x = 1_ SF by Th9;