let Y be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st f | Y is constant holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V st f | Y is constant holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V st f | Y is constant holds
( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )
let f be PartFunc of C,V; :: thesis: ( f | Y is constant implies ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded ) )
assume A1: f | Y is constant ; :: thesis: ( ( for r being Real holds r (#) f is_bounded_on Y ) & - f is_bounded_on Y & ||.f.|| | Y is bounded )

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

let r be Real; :: thesis: r (#) f is_bounded_on Y
(r (#) f) | Y is constant by A1, Th52;
hence r (#) f is_bounded_on Y by Th54; :: thesis: verum

end;

(- f) | Y is constant by A1, Th53;
hence - f is_bounded_on Y by Th54; :: thesis: ||.f.|| | Y is bounded
||.f.|| | Y is constant by A1, Th53;
hence ||.f.|| | Y is bounded ; :: thesis: verum