let Z be RealNormSpace; :: thesis: for X, Y being set

for f1, f2 being PartFunc of REAL, the carrier of Z 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, the carrier of Z 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, the carrier of Z; :: 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 b_{1} being set holds

( not b_{1} in dom ((f1 - f2) | (X /\ Y)) or not r1 + r2 <= ||.(((f1 - f2) | (X /\ Y)) /. b_{1}).|| )

let x be set ; :: thesis: ( not x in dom ((f1 - f2) | (X /\ Y)) or not r1 + r2 <= ||.(((f1 - f2) | (X /\ Y)) /. x).|| )

assume A8: x in dom ((f1 - f2) | (X /\ Y)) ; :: thesis: not r1 + r2 <= ||.(((f1 - f2) | (X /\ Y)) /. x).||

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 & x in X & x in Y ) by A8, XBOOLE_0:def 4;

then A11: x in dom (f2 | Y) by RELAT_1:57;

((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, PARTFUN2:17

.= ((f1 | X) /. x) - ((f2 | Y) /. x) by A10, PARTFUN2:17 ;

then A12: ||.(((f1 - f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:3;

||.((f1 | X) /. x).|| < r1 by A2, A10, RELAT_1:57;

then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A11, 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, the carrier of Z 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, the carrier of Z 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, the carrier of Z; :: 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 A41: 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 & x in X & x in Y ) by A41, XBOOLE_0:def 4;

then A6: x in dom (f2 | Y) by RELAT_1:57;

((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, PARTFUN2:17

.= ((f1 | X) /. x) + ((f2 | Y) /. x) by A5, PARTFUN2:17 ;

then A7: ||.(((f1 + f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:def 1;

||.((f1 | X) /. x).|| < r1 by A2, A5, RELAT_1:57;

then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A3, A6, XREAL_1:8;

hence ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 by A7, XXREAL_0:2; :: thesis: verum

end;assume A41: 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 & x in X & x in Y ) by A41, XBOOLE_0:def 4;

then A6: x in dom (f2 | Y) by RELAT_1:57;

((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, PARTFUN2:17

.= ((f1 | X) /. x) + ((f2 | Y) /. x) by A5, PARTFUN2:17 ;

then A7: ||.(((f1 + f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:def 1;

||.((f1 | X) /. x).|| < r1 by A2, A5, RELAT_1:57;

then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A3, A6, 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 b

( not b

let x be set ; :: thesis: ( not x in dom ((f1 - f2) | (X /\ Y)) or not r1 + r2 <= ||.(((f1 - f2) | (X /\ Y)) /. x).|| )

assume A8: x in dom ((f1 - f2) | (X /\ Y)) ; :: thesis: not r1 + r2 <= ||.(((f1 - f2) | (X /\ Y)) /. x).||

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 & x in X & x in Y ) by A8, XBOOLE_0:def 4;

then A11: x in dom (f2 | Y) by RELAT_1:57;

((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, PARTFUN2:17

.= ((f1 | X) /. x) - ((f2 | Y) /. x) by A10, PARTFUN2:17 ;

then A12: ||.(((f1 - f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:3;

||.((f1 | X) /. x).|| < r1 by A2, A10, RELAT_1:57;

then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A11, A3, XREAL_1:8;

hence ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 by A12, XXREAL_0:2; :: thesis: verum