theorem :: VECTSP_2:16

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