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 ;

(- 1r) (#) f is_bounded_on Y by A1, Th44;

hence - f is_bounded_on Y by Th23; :: thesis: verum

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

hence
||.f.|| | Y is bounded
by RFUNCT_1:73; :: thesis: - f is_bounded_on Y|.(||.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;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

(- 1r) (#) f is_bounded_on Y by A1, Th44;

hence - f is_bounded_on Y by Th23; :: thesis: verum