let SF be Skew-Field; :: thesis: for y, x being Scalar of SF st y <> 0. SF holds
(x / y) * y = x
let y, x 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, Th43
.= x by VECTSP_1:def 4 ; :: thesis: verum