let SF be Skew-Field; :: thesis: for y, z, x being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / y = (x * z) / (y * z)
let y, z, x be Scalar of SF; :: thesis: ( y <> 0. SF & z <> 0. SF implies x / y = (x * z) / (y * z) )
assume A1: y <> 0. SF ; :: thesis: ( not z <> 0. SF or x / y = (x * z) / (y * z) )
assume A2: z <> 0. SF ; :: thesis: x / y = (x * z) / (y * z)
thus x / y = (x * (1_ SF)) * (y " ) by VECTSP_1:def 13
.= (x * (z * (z " ))) * (y " ) by A2, Th43
.= ((x * z) * (z " )) * (y " ) by GROUP_1:def 4
.= (x * z) * ((z " ) * (y " )) by GROUP_1:def 4
.= (x * z) / (y * z) by A1, A2, Th46 ; :: thesis: verum