set f = X --> (0. Y);

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

for x being Element of X holds f . x = 0. Y by FUNCOP_1:7;

then f is bounded by Th6;

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

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

for x being Element of X holds f . x = 0. Y by FUNCOP_1:7;

then f is bounded by Th6;

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