let c, d, a, b be complex number ; :: thesis: ( c <> 0 & d <> 0 & a / d = b / c implies a * c = b * d )
assume A1: ( c <> 0 & d <> 0 & a / d = b / c ) ; :: thesis: a * c = b * d
then c * (a / d) = b by Lm3;
then (a * c) / d = b by Lm9;
hence a * c = b * d by A1, Lm3; :: thesis: verum