let a, b, e be Complex; :: thesis: ( b <> 0 implies (a / b) - e = (a - (e * b)) / b )
assume A1: b <> 0 ; :: thesis: (a / b) - e = (a - (e * b)) / b
thus (a / b) - e = (a / b) + (- e)
.= (a + ((- e) * b)) / b by A1, Th113
.= (a - (e * b)) / b ; :: thesis: verum