let a, b, c, d be Complex; ( c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c )
assume that
A1:
c <> 0
and
A2:
d <> 0
; ( not a * c = b * d or a / d = b / c )
assume
a * c = b * d
; 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; verum