let a, b, c be Complex; :: thesis: ( c <> 0 implies a + b = ((a * c) + (b * c)) / c )
assume A1: c <> 0 ; :: thesis: a + b = ((a * c) + (b * c)) / c
hence a + b = ((a * c) / c) + b by Lm9
.= ((a * c) / c) + ((b * c) / c) by A1, Lm9
.= ((a * c) + (b * c)) / c by Th62 ;
:: thesis: verum