reconsider
f
=
f
as
BilinearOperator
of
X
,
Y
,
Z
by
Def9
;
f
.
(
v
,
w
) is
VECTOR
of
Z
;
hence
f
.
(
v
,
w
) is
VECTOR
of
Z
;
:: thesis:
verum