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 V8() 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 V8() 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 V8() 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 V8() 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 V8() ; :: 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 V8() by A1, Th52;
hence r (#) f is_bounded_on Y by Th54; :: thesis: verum
end;
(- f) | Y is V8() by A1, Th53;
hence - f is_bounded_on Y by Th54; :: thesis: ||.f.|| | Y is bounded
||.f.|| | Y is V8() by A1, Th53;
hence ||.f.|| | Y is bounded ; :: thesis: verum