let
x
be
Complex
;
:: thesis:
x

0
=
x
x

0
=
x
+
0
by
Lm1
,
XCMPLX_0:def 8
;
hence
x

0
=
x
by
Th1
;
:: thesis:
verum