set
g
=
[:
the
carrier
of
E
, the
carrier
of
F
:]
-->
(
0.
G
)
;
reconsider
f
=
[:
the
carrier
of
E
, the
carrier
of
F
:]
-->
(
0.
G
)
as
Function
of
[:
E
,
F
:]
,
G
;
take
f
;
:: thesis:
f
is
Bilinear
thus
f
is
Bilinear
by
EX1
;
:: thesis:
verum