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 ;

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

hence
(- f) | X is bounded
; :: thesis: verum||.(((- 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;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