set f = the carrier of (product X) --> (0. Y);
reconsider f = the carrier of (product X) --> (0. Y) as MultilinearOperator of X,Y by Th19;
for x being VECTOR of (product X) holds f . x = 0. Y by FUNCOP_1:7;
then f is Lipschitzian by Th21;
hence not BoundedMultilinearOperators (X,Y) is empty by Def9; :: thesis: verum