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

g
)
*'
=
(
f
*'
)

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

g
)
*'
=
(
f
*'
)

(
g
*'
)
thus
(
f

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

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

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