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