let Y be set ; :: thesis: for C being non empty set

for f being PartFunc of C,REAL st f | Y is constant holds

( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )

let C be non empty set ; :: thesis: for f being PartFunc of C,REAL st f | Y is constant holds

( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )

let f be PartFunc of C,REAL; :: thesis: ( f | Y is constant implies ( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) )

assume A1: f | Y is constant ; :: thesis: ( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )

hence (- f) | Y is bounded ; :: thesis: (abs f) | Y is bounded

(abs f) | Y is constant by A1, Th91;

hence (abs f) | Y is bounded ; :: thesis: verum

for f being PartFunc of C,REAL st f | Y is constant holds

( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )

let C be non empty set ; :: thesis: for f being PartFunc of C,REAL st f | Y is constant holds

( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )

let f be PartFunc of C,REAL; :: thesis: ( f | Y is constant implies ( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) )

assume A1: f | Y is constant ; :: thesis: ( ( for r being Real holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded )

hereby :: thesis: ( (- f) | Y is bounded & (abs f) | Y is bounded )

(- f) | Y is constant
by A1, Th90;let r be Real; :: thesis: (r (#) f) | Y is bounded

(r (#) f) | Y is constant by A1, Th89;

hence (r (#) f) | Y is bounded ; :: thesis: verum

end;(r (#) f) | Y is constant by A1, Th89;

hence (r (#) f) | Y is bounded ; :: thesis: verum

hence (- f) | Y is bounded ; :: thesis: (abs f) | Y is bounded

(abs f) | Y is constant by A1, Th91;

hence (abs f) | Y is bounded ; :: thesis: verum