let SF be Skew-Field; :: thesis: for x, y, z being Scalar of SF st y <> 0. SF & z <> 0. SF holds
x / (y / z) = (x * z) / y
let x, y, z be Scalar of SF; :: thesis: ( y <> 0. SF & z <> 0. SF implies x / (y / z) = (x * z) / y )
assume A1: y <> 0. SF ; :: thesis: ( not z <> 0. SF or x / (y / z) = (x * z) / y )
assume A2: z <> 0. SF ; :: thesis: x / (y / z) = (x * z) / y
then z " <> 0. SF by Th13;
hence x / (y / z) = x * (((z ") ") * (y ")) by A1, Th11
.= x * (z * (y ")) by A2, Th14
.= (x * z) / y by GROUP_1:def 3 ;
:: thesis: verum