theorem Th19: :: LOPBAN_1:19

for X, Y being RealLinearSpace holds the carrier of X --> (0. Y) is LinearOperator of X,Y