let c, d, a, b be complex number ; :: thesis: ( c <> 0 & d <> 0 & a * c = b / d implies a * d = b / c )
assume A1: ( c <> 0 & 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 * c) * d = b by A1, Lm3;
then (a * d) * c = b ;
hence a * d = b / c by A1, Lm10; :: thesis: verum