[: the carrier of E, the carrier of F:] --> (0. G) is Bilinear by EX1;
hence ex b₁ being Function of [: the carrier of E, the carrier of F:], the carrier of G st b₁ is Bilinear ; :: thesis: verum