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

proof

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

end;

hence not ComplexBoundedFunctions X,Y is empty by Def5; :: thesis: verum