let b, d, a, e be complex number ; :: thesis: ( b <> 0 & d <> 0 & b <> d & a / b = e / d implies a / b = (a - e) / (b - d) )
assume A1: ( b <> 0 & d <> 0 & b <> d & a / b = e / d ) ; :: thesis: a / b = (a - e) / (b - d)
then A2: b - d <> 0 ;
a * d = e * b by A1, Th96;
then a * (b - d) = (a - e) * b ;
hence a / b = (a - e) / (b - d) by A1, A2, Th95; :: thesis: verum