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

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

hence
0c (#) f is_bounded_on Y
; :: thesis: verumfor 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;||.((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