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
( | 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
( | 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
( | Y is bounded & - f is_bounded_on Y )

let Y be set ; :: thesis: ( f is_bounded_on Y implies ( | Y is bounded & - f is_bounded_on Y ) )
assume A1: f is_bounded_on Y ; :: thesis: ( | 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 /\ () holds
|.( . c).| <= r1
let c be object ; :: thesis: ( c in Y /\ () implies |.( . c).| <= r1 )
assume A3: c in Y /\ () ; :: thesis: |.( . c).| <= r1
then A4: c in Y by XBOOLE_0:def 4;
A5: c in dom by ;
then c in dom f by NORMSP_0:def 3;
then c in Y /\ (dom f) by ;
then ( ||.(f /. c).|| >= 0 & ||.(f /. c).|| <= r1 ) by ;
then |.||.(f /. c).||.| <= r1 by ABSVALUE:def 1;
hence |.( . c).| <= r1 by ; :: thesis: verum
end;
hence ||.f.|| | Y is bounded by RFUNCT_1:73; :: thesis:
(- 1r) (#) f is_bounded_on Y by ;
hence - f is_bounded_on Y by Th23; :: thesis: verum