let a, b, c be Complex; ( b <> 0 implies c - (a / b) = ((c * b) - a) / b )
assume A1:
b <> 0
; c - (a / b) = ((c * b) - a) / b
thus c - (a / b) =
- ((a / b) - c)
.=
- ((a - (c * b)) / b)
by A1, Th126
.=
(- (a - (c * b))) / b
by Lm17
.=
((c * b) - a) / b
; verum