let SF be Skew-Field; :: thesis: for x, y being Scalar of SF st y * x = 1_ SF holds
( x = y " & y = x " )
let x, y be Scalar of SF; :: thesis: ( y * x = 1_ SF implies ( x = y " & y = x " ) )
A1: ( y * x = 1_ SF implies y = x " )

proof

assume A2: y * x = 1_ SF ; :: thesis: y = x "
then x <> 0. SF ;
hence y = x " by A2, Def2; :: thesis: verum

end;

( y * x = 1_ SF implies x = y " )

proof

assume y * x = 1_ SF ; :: thesis: x = y "
then ( y <> 0. SF & x * y = 1_ SF ) by Th7;
hence x = y " by Def2; :: thesis: verum

end;

hence ( y * x = 1_ SF implies ( x = y " & y = x " ) ) by A1; :: thesis: verum