let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set holds 0c (#) f is_bounded_on Y
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for Y being set holds 0c (#) f is_bounded_on Y
let f be PartFunc of M,V; :: thesis: for Y being set holds 0c (#) f is_bounded_on Y
let Y be set ; :: thesis: 0c (#) f is_bounded_on Y
now :: thesis: ex p being Element of NAT st
for c being Element of M st c in Y /\ (dom (0c (#) f)) holds
||.((0c (#) f) /. c).|| <= p
take p = 0 ; :: thesis: for c being Element of M st c in Y /\ (dom (0c (#) f)) holds
||.((0c (#) f) /. c).|| <= p
let c be Element of M; :: thesis: ( c in Y /\ (dom (0c (#) f)) implies ||.((0c (#) f) /. c).|| <= p )
|.0c.| * ||.(f /. c).|| <= 0 by COMPLEX1:44;
then A1: ||.(0c * (f /. c)).|| <= 0 by CLVECT_1:def 13;
assume c in Y /\ (dom (0c (#) f)) ; :: thesis: ||.((0c (#) f) /. c).|| <= p
then c in dom (0c (#) f) by XBOOLE_0:def 4;
hence ||.((0c (#) f) /. c).|| <= p by A1, Def2; :: thesis: verum
end;
hence 0c (#) f is_bounded_on Y ; :: thesis: verum