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))
thus a - b = a + (- b)
.= a * (1 + ((- b) / a)) by A1, Th117
.= a * (1 + (- (b / a))) by Lm17
.= a * (1 - (b / a)) ; :: thesis: verum