set f = the carrier of X --> (0. Y);
reconsider f = the carrier of X --> (0. Y) as LinearOperator of X,Y by Th18;
for x being VECTOR of X holds f . x = 0. Y by FUNCOP_1:7;
then f is Lipschitzian by Th20;
hence not BoundedLinearOperators (X,Y) is empty by Def7; :: thesis: verum