for X, Y, Z being RealLinearSpace holds the carrier of [:X,Y:] --> (0. Z) is BilinearOperator of X,Y,Z by LOPBAN_8:9, LOPBAN_8:def 2;