set f = X --> (0. Y);
reconsider f = X --> (0. Y) as Function of X, the carrier of Y ;
take f ; :: thesis: f is bounded
for x being Element of X holds f . x = 0. Y by FUNCOP_1:7;
hence f is bounded by Th5; :: thesis: verum