let Z be RealNormSpace; :: thesis: for X being set
for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(- f) | X is bounded
let X be set ; :: thesis: for f being PartFunc of REAL, the carrier of Z st f | X is bounded holds
(- f) | X is bounded
let f be PartFunc of REAL, the carrier of Z; :: thesis: ( f | X is bounded implies (- f) | X is bounded )
assume f | X is bounded ; :: thesis: (- f) | X is bounded
then consider s being Real such that
A2: for x being set st x in dom (f | X) holds
||.((f | X) /. x).|| < s ;

now :: thesis: for x being set st x in dom ((- f) | X) holds
||.(((- f) | X) /. x).|| < s

let x be set ; :: thesis: ( x in dom ((- f) | X) implies ||.(((- f) | X) /. x).|| < s )
assume x in dom ((- f) | X) ; :: thesis: ||.(((- f) | X) /. x).|| < s
then A4: x in dom (- (f | X)) by VFUNCT_1:29;
then x in dom (f | X) by VFUNCT_1:def 5;
then A5: ||.((f | X) /. x).|| < s by A2;
((- f) | X) /. x = (- (f | X)) /. x by VFUNCT_1:29
.= - ((f | X) /. x) by A4, VFUNCT_1:def 5 ;
hence ||.(((- f) | X) /. x).|| < s by A5, NORMSP_1:2; :: thesis: verum

end;

hence (- f) | X is bounded ; :: thesis: verum