let n be Element of NAT ; :: thesis: for X, Y being set
for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds
( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let X, Y be set ; :: thesis: for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds
( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let f1, f2 be PartFunc of REAL,(REAL-NS n); :: thesis: ( f1 | X is bounded & f2 | Y is bounded implies ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) )
assume A1: ( f1 | X is bounded & f2 | Y is bounded ) ; :: thesis: ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
consider r1 being Real such that
A2: for x being set st x in dom (f1 | X) holds
||.((f1 | X) /. x).|| < r1 by A1;
consider r2 being Real such that
A3: for x being set st x in dom (f2 | Y) holds
||.((f2 | Y) /. x).|| < r2 by A1;

now :: thesis: for x being set st x in dom ((f1 + f2) | (X /\ Y)) holds
||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2

let x be set ; :: thesis: ( x in dom ((f1 + f2) | (X /\ Y)) implies ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 )
assume x in dom ((f1 + f2) | (X /\ Y)) ; :: thesis: ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2
then A4: ( x in dom (f1 + f2) & x in X /\ Y ) by RELAT_1:57;
then x in (dom f1) /\ (dom f2) by VFUNCT_1:def 1;
then A5: ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def 4;
A6: ( x in X & x in Y ) by A4, XBOOLE_0:def 4;
((f1 + f2) | (X /\ Y)) /. x = (f1 + f2) /. x by A4, PARTFUN2:17
.= (f1 /. x) + (f2 /. x) by A4, VFUNCT_1:def 1
.= ((f1 | X) /. x) + (f2 /. x) by A5, A6, PARTFUN2:17
.= ((f1 | X) /. x) + ((f2 | Y) /. x) by A5, A6, PARTFUN2:17 ;
then A7: ||.(((f1 + f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:def 1;
x in dom (f1 | X) by A5, A6, RELAT_1:57;
then A8: ||.((f1 | X) /. x).|| < r1 by A2;
x in dom (f2 | Y) by A5, A6, RELAT_1:57;
then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A3, A8, XREAL_1:8;
hence ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 by A7, XXREAL_0:2; :: thesis: verum

end;

hence (f1 + f2) | (X /\ Y) is bounded ; :: thesis: (f1 - f2) | (X /\ Y) is bounded
take r1 + r2 ; :: according to INTEGR19:def 1 :: thesis: for y being set st y in dom ((f1 - f2) | (X /\ Y)) holds
||.(((f1 - f2) | (X /\ Y)) /. y).|| < r1 + r2
let x be set ; :: thesis: ( x in dom ((f1 - f2) | (X /\ Y)) implies ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 )
assume x in dom ((f1 - f2) | (X /\ Y)) ; :: thesis: ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2
then A9: ( x in dom (f1 - f2) & x in X /\ Y ) by RELAT_1:57;
then x in (dom f1) /\ (dom f2) by VFUNCT_1:def 2;
then A10: ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def 4;
A11: ( x in X & x in Y ) by A9, XBOOLE_0:def 4;
((f1 - f2) | (X /\ Y)) /. x = (f1 - f2) /. x by A9, PARTFUN2:17
.= (f1 /. x) - (f2 /. x) by A9, VFUNCT_1:def 2
.= ((f1 | X) /. x) - (f2 /. x) by A10, A11, PARTFUN2:17
.= ((f1 | X) /. x) - ((f2 | Y) /. x) by A10, A11, PARTFUN2:17 ;
then A12: ||.(((f1 - f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:3;
x in dom (f1 | X) by A10, A11, RELAT_1:57;
then A13: ||.((f1 | X) /. x).|| < r1 by A2;
x in dom (f2 | Y) by A10, A11, RELAT_1:57;
then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A13, A3, XREAL_1:8;
hence ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 by A12, XXREAL_0:2; :: thesis: verum