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