let X, Y be set ; :: thesis: for C being non empty set
for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
(f1 + f2) | (X /\ Y) is bounded
let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds
(f1 + f2) | (X /\ Y) is bounded
let f1, f2 be PartFunc of C,COMPLEX; :: thesis: ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded )
assume that
A1: f1 | X is bounded and
A2: f2 | Y is bounded ; :: thesis: (f1 + f2) | (X /\ Y) is bounded
consider r1 being Real such that
A3: for c being Element of C st c in X /\ (dom f1) holds
|.(f1 /. c).| <= r1 by A1, Th68;
consider r2 being Real such that
A4: for c being Element of C st c in Y /\ (dom f2) holds
|.(f2 /. c).| <= r2 by A2, Th68;
ex p1 being Real st
for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds
|.((f1 + f2) /. c).| <= p1
proof
take r0 = r1 + r2; :: thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds
|.((f1 + f2) /. c).| <= r0
let c be Element of C; :: thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies |.((f1 + f2) /. c).| <= r0 )
A5: |.((f1 /. c) + (f2 /. c)).| <= |.(f1 /. c).| + |.(f2 /. c).| by COMPLEX1:56;
assume A6: c in (X /\ Y) /\ (dom (f1 + f2)) ; :: thesis: |.((f1 + f2) /. c).| <= r0
then A7: c in X /\ Y by XBOOLE_0:def 4;
then A8: c in X by XBOOLE_0:def 4;
A9: c in Y by A7, XBOOLE_0:def 4;
A10: c in dom (f1 + f2) by A6, XBOOLE_0:def 4;
then A11: c in (dom f1) /\ (dom f2) by VALUED_1:def 1;
then c in dom f2 by XBOOLE_0:def 4;
then c in Y /\ (dom f2) by A9, XBOOLE_0:def 4;
then A12: |.(f2 /. c).| <= r2 by A4;
c in dom f1 by A11, XBOOLE_0:def 4;
then c in X /\ (dom f1) by A8, XBOOLE_0:def 4;
then |.(f1 /. c).| <= r1 by A3;
then |.(f1 /. c).| + |.(f2 /. c).| <= r0 by A12, XREAL_1:7;
then |.((f1 /. c) + (f2 /. c)).| <= r0 by A5, XXREAL_0:2;
hence |.((f1 + f2) /. c).| <= r0 by A10, Th1; :: thesis: verum
end;
hence (f1 + f2) | (X /\ Y) is bounded by Th68; :: thesis: verum