let a, b, c, d be Complex; :: thesis: ( c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c )
assume that
A1: c <> 0 and
A2: d <> 0 ; :: thesis: ( not a * c = b * d or a / d = b / c )
assume a * c = b * d ; :: thesis: a / d = b / c
then a = (b * d) / c by A1, Lm9;
then a = d * (b / c) by Lm8;
hence a / d = b / c by A2, Lm9; :: thesis: verum