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