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