set f = the carrier of X --> (0. Y);
reconsider f = the carrier of X --> (0. Y) as LinearOperator of X,Y by Th21;
f is bounded

proof

for x being VECTOR of X holds f . x = 0. Y by FUNCOP_1:13;
hence f is bounded by Th23; :: thesis: verum

end;

hence not BoundedLinearOperators X,Y is empty by Def8; :: thesis: verum