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 * c) * d = b by A2, Lm3;
then (a * d) * c = b ;
hence a * d = b / c by A1, Lm9; :: thesis: verum