theorem Th9: :: VECTSP_2:9

for SF being Skew-Field
for x being Scalar of SF st x <> 0. SF holds
( x * (x ") = 1. SF & (x ") * x = 1. SF )