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

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

take p = |.r.|; :: thesis: for c being Element of C st c in Y /\ (dom f) holds
|.(f /. c).| <= p
let c be Element of C; :: 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 | Y is bounded by Th68; :: thesis: verum