theorem Th11: :: VECTSP_2:11

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