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;

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

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

hence
(f1 + f2) | (X /\ Y) is bounded
; :: thesis: (f1 - f2) | (X /\ Y) is bounded ||.(((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;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

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