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