theorem Th10: :: VECTSP_2:10

for SF being Skew-Field
for x, y being Scalar of SF st y * x = 1_ SF holds
( x = y " & y = x " )