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