let SF be Skew-Field; :: thesis: for x, y being Scalar of SF st y <> 0. SF holds
(x / y) * y = x
let x, y be Scalar of SF; :: thesis: ( y <> 0. SF implies (x / y) * y = x )
assume A1: y <> 0. SF ; :: thesis: (x / y) * y = x
thus (x / y) * y = x * ((y ") * y) by GROUP_1:def 3
.= x * (1_ SF) by A1, Th9
.= x ; :: thesis: verum