let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let f be PartFunc of M,V; :: thesis: for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded & - f is_bounded_on Y )
let Y be set ; :: thesis: ( f is_bounded_on Y implies ( ||.f.|| | Y is bounded & - f is_bounded_on Y ) )
assume A1: f is_bounded_on Y ; :: thesis: ( ||.f.|| | Y is bounded & - f is_bounded_on Y )
then consider r1 being Real such that
A2: for c being Element of M st c in Y /\ (dom f) holds
||.(f /. c).|| <= r1 ;

now :: thesis: for c being object st c in Y /\ (dom ||.f.||) holds
|.(||.f.|| . c).| <= r1

let c be object ; :: thesis: ( c in Y /\ (dom ||.f.||) implies |.(||.f.|| . c).| <= r1 )
assume A3: c in Y /\ (dom ||.f.||) ; :: thesis: |.(||.f.|| . c).| <= r1
then A4: c in Y by XBOOLE_0:def 4;
A5: c in dom ||.f.|| by A3, XBOOLE_0:def 4;
then c in dom f by NORMSP_0:def 3;
then c in Y /\ (dom f) by A4, XBOOLE_0:def 4;
then ( ||.(f /. c).|| >= 0 & ||.(f /. c).|| <= r1 ) by A2, CLVECT_1:105;
then |.||.(f /. c).||.| <= r1 by ABSVALUE:def 1;
hence |.(||.f.|| . c).| <= r1 by A5, NORMSP_0:def 3; :: thesis: verum

end;

hence ||.f.|| | Y is bounded by RFUNCT_1:73; :: thesis: - f is_bounded_on Y
(- 1r) (#) f is_bounded_on Y by A1, Th44;
hence - f is_bounded_on Y by Th23; :: thesis: verum