let
V
be non
empty
ModuleStr
over
F_Complex
;
:: thesis:
for
f
,
g
being
Functional
of
V
holds
(
f

g
)
*'
=
(
f
*'
)

(
g
*'
)
let
f
,
g
be
Functional
of
V
;
:: thesis:
(
f

g
)
*'
=
(
f
*'
)

(
g
*'
)
thus
(
f

g
)
*'
=
(
f
*'
)
+
(
(

g
)
*'
)
by
Th18
.=
(
f
*'
)

(
g
*'
)
by
Th19
;
:: thesis:
verum