let
v
be
Vector
of
V
;
:: according to
BILINEAR:def 26
:: thesis:
(
f
+
g
)
.
(
v
,
v
)
=
0.
K
thus
(
f
+
g
)
.
(
v
,
v
) =
(
f
.
(
v
,
v
)
)
+
(
g
.
(
v
,
v
)
)
by
Def2
.=
(
0.
K
)
+
(
g
.
(
v
,
v
)
)
by
Def26
.=
(
0.
K
)
+
(
0.
K
)
by
Def26
.=
0.
K
by
RLVECT_1:def 4
;
:: thesis:
verum