reconsider
x1
=
x
,
y1
=
y
as
Complex
by
A1
;
take
x1
+
y1
;
:: thesis:
ex
x1
,
y1
being
Complex
st
(
x1
=
x
&
y1
=
y
&
x1
+
y1
=
x1
+
y1
)
thus
ex
x1
,
y1
being
Complex
st
(
x1
=
x
&
y1
=
y
&
x1
+
y1
=
x1
+
y1
) ;
:: thesis:
verum