let SF be Skew-Field; :: thesis: for x, y, z being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / y = (x * z) / (y * z)
let x, y, z 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 ")
.= (x * (z * (z "))) * (y ") by A2, Th9
.= ((x * z) * (z ")) * (y ") by GROUP_1:def 3
.= (x * z) * ((z ") * (y ")) by GROUP_1:def 3
.= (x * z) / (y * z) by A1, A2, Th11 ; :: thesis: verum