let n be Element of NAT ; :: thesis: for X, Y being set
for f1, f2 being PartFunc of REAL,() 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,() 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,(); :: 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 ;
((f1 + f2) | (X /\ Y)) /. x = (f1 + f2) /. x by
.= (f1 /. x) + (f2 /. x) by
.= ((f1 | X) /. x) + (f2 /. x) by
.= ((f1 | X) /. x) + ((f2 | Y) /. x) by ;
then A7: ||.(((f1 + f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:def 1;
x in dom (f1 | X) by ;
then A8: ||.((f1 | X) /. x).|| < r1 by A2;
x in dom (f2 | Y) by ;
then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by ;
hence ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 by ; :: 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 ;
((f1 - f2) | (X /\ Y)) /. x = (f1 - f2) /. x by
.= (f1 /. x) - (f2 /. x) by
.= ((f1 | X) /. x) - (f2 /. x) by
.= ((f1 | X) /. x) - ((f2 | Y) /. x) by ;
then A12: ||.(((f1 - f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:3;
x in dom (f1 | X) by ;
then A13: ||.((f1 | X) /. x).|| < r1 by A2;
x in dom (f2 | Y) by ;
then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by ;
hence ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 by ; :: thesis: verum