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