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