let
v
,
w
be
Vector
of
V
;
:: according to
BILINEAR:def 25
:: thesis:
(
a
*
f
)
.
(
v
,
w
)
=
(
a
*
f
)
.
(
w
,
v
)
thus
(
a
*
f
)
.
(
v
,
w
) =
a
*
(
f
.
(
v
,
w
)
)
by
Def3
.=
a
*
(
f
.
(
w
,
v
)
)
by
Def25
.=
(
a
*
f
)
.
(
w
,
v
)
by
Def3
;
:: thesis:
verum