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