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;
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 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;
hence (f1 + f2) | (X /\ Y) is bounded ; :: thesis: (f1 - f2) | (X /\ Y) is bounded
take r1 + r2 ; :: according to INTEGR19:def 1 :: thesis: for b1 being set holds
( not b1 in dom ((f1 - f2) | (X /\ Y)) or not r1 + r2 <= ||.(((f1 - f2) | (X /\ Y)) /. b1).|| )
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