let a, b be Complex; :: thesis: ( b <> 0 implies ex e being Complex st a = b / e )
assume A1: b <> 0 ; :: thesis: ex e being Complex st a = b / e

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

suppose A2: a = 0 ; :: thesis: ex e being Complex st a = b / e

take 0 ; :: thesis: a = b / 0
b / 0 = b * (0 ") by XCMPLX_0:def 9;
hence a = b / 0 by A2; :: thesis: verum

end;

suppose A3: a <> 0 ; :: thesis: ex e being Complex st a = b / e

take e = b / a; :: thesis: a = b / e
thus a = a * 1
.= a * (e * (e ")) by A1, A3, XCMPLX_0:def 7
.= (a * e) * (e ")
.= (a * ((a ") * b)) * (e ") by XCMPLX_0:def 9
.= ((a * (a ")) * b) * (e ")
.= (1 * b) * (e ") by A3, XCMPLX_0:def 7
.= b / e by XCMPLX_0:def 9 ; :: thesis: verum

end;

end;