let a, b, d, e be Complex; :: thesis: ( b <> 0 & d <> 0 & b <> d & a / b = e / d implies a / b = (a - e) / (b - d) )
assume that
A1: b <> 0 and
A2: d <> 0 and
A3: b <> d and
A4: a / b = e / d ; :: thesis: a / b = (a - e) / (b - d)
a * d = e * b by A1, A2, A4, Th95;
then A5: a * (b - d) = (a - e) * b ;
b - d <> 0 by A3;
hence a / b = (a - e) / (b - d) by A1, A5, Th94; :: thesis: verum