let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,the carrier of 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,the carrier of 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,the carrier of 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 by Def7;

now

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

end;

hence ||.f.|| | Y is bounded by RFUNCT_1:90; :: 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