let
c1
,
c2
be
Complex
;
:: thesis:
Sum
<*
c1
,
c2
*>
=
c1
+
c2
reconsider
s1
=
c1
as
Element
of
COMPLEX
by
XCMPLX_0:def 2
;
thus
Sum
<*
c1
,
c2
*>
=
(
Sum
<*
s1
*>
)
+
c2
by
Th31
.=
c1
+
c2
by
FINSOP_1:11
;
:: thesis:
verum