let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
f is_bounded_on Y
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for Y being set st f | Y is constant holds
f is_bounded_on Y
let f be PartFunc of M,V; :: thesis: for Y being set st f | Y is constant holds
f is_bounded_on Y
let Y be set ; :: thesis: ( f | Y is constant implies f is_bounded_on Y )
assume f | Y is constant ; :: thesis: f is_bounded_on Y
then consider r being VECTOR of V such that
A1: for c being Element of M st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;

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

reconsider p = ||.r.|| as Real ;
take p = p; :: thesis: for c being Element of M st c in Y /\ (dom f) holds
||.(f /. c).|| <= p
let c be Element of M; :: thesis: ( c in Y /\ (dom f) implies ||.(f /. c).|| <= p )
assume c in Y /\ (dom f) ; :: thesis: ||.(f /. c).|| <= p
hence ||.(f /. c).|| <= p by A1; :: thesis: verum

end;

hence f is_bounded_on Y ; :: thesis: verum