let Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st f | Y is constant holds
( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds
( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
let f be PartFunc of C,COMPLEX; :: thesis: ( f | Y is constant implies ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded ) )
assume A1: f | Y is constant ; :: thesis: ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded )
hence for r being Element of COMPLEX holds (r (#) f) | Y is bounded by Th91, Th93; :: thesis: ( (- f) | Y is bounded & |.f.| | Y is bounded )
thus (- f) | Y is bounded by A1, Th92, Th93; :: thesis: |.f.| | Y is bounded
|.f.| | Y is constant by A1, Th92;
hence |.f.| | Y is bounded ; :: thesis: verum