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