theorem EX1: :: LOPBAN_8:9

for E, F, G being RealLinearSpace holds [: the carrier of E, the carrier of F:] --> (0. G) is Bilinear