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