let a, b, c, d be Complex; :: thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)

per cases ( b = 0 or b <> 0 ) ;

suppose A1: b = 0 ; :: thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)

A2: a / b = a * (b ") by XCMPLX_0:def 9
.= a * 0 by A1 ;
thus (((d - c) / b) * a) + c = (((d - c) * (b ")) * a) + c by XCMPLX_0:def 9
.= (((d - c) * 0) * a) + c by A1
.= ((1 - (a / b)) * c) + ((a / b) * d) by A2 ; :: thesis: verum

end;

suppose A3: b <> 0 ; :: thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)

(((d - c) / b) * a) + c = (((d - c) / b) * a) + (c * 1)
.= (((d - c) / b) * a) + (c * (b / b)) by A3, Lm5
.= (((d - c) / b) * a) + ((c * b) / b) by Lm8
.= (((d - c) * a) / b) + ((c * b) / b) by Lm8
.= (((d - c) * a) + (c * b)) / b by Th62
.= (((b - a) * c) + (a * d)) / b
.= (((b - a) * c) / b) + ((a * d) / b) by Th62
.= (((b - a) * c) / b) + ((a / b) * d) by Lm8
.= (((b - a) / b) * c) + ((a / b) * d) by Lm8
.= (((b / b) - (a / b)) * c) + ((a / b) * d) by Th120
.= ((1 - (a / b)) * c) + ((a / b) * d) by A3, Lm5 ;
hence (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d) ; :: thesis: verum

end;

end;