let Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y
let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V holds 0 (#) f is_bounded_on Y
let f be PartFunc of C,V; :: thesis: 0 (#) f is_bounded_on Y

now :: thesis: ex p being Element of NAT st
for c being Element of C st c in Y /\ (dom (0 (#) f)) holds
||.((0 (#) f) /. c).|| <= p

take p = 0 ; :: thesis: for c being Element of C st c in Y /\ (dom (0 (#) f)) holds
||.((0 (#) f) /. c).|| <= p
let c be Element of C; :: thesis: ( c in Y /\ (dom (0 (#) f)) implies ||.((0 (#) f) /. c).|| <= p )
0 * ||.(f /. c).|| = 0 ;
then |.0.| * ||.(f /. c).|| <= 0 by ABSVALUE:2;
then A1: ||.(0 * (f /. c)).|| <= 0 by NORMSP_1:def 1;
assume c in Y /\ (dom (0 (#) f)) ; :: thesis: ||.((0 (#) f) /. c).|| <= p
then c in dom (0 (#) f) by XBOOLE_0:def 4;
hence ||.((0 (#) f) /. c).|| <= p by A1, Def4; :: thesis: verum

end;

hence 0 (#) f is_bounded_on Y ; :: thesis: verum