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 A1: ( f1 | X is bounded & f2 | Y is bounded ) ; :: thesis: (f1 + f2) | (X /\ Y) is bounded
then consider r1 being real number such that
A2: for c being Element of C st c in X /\ (dom f1) holds
|.(f1 /. c).| <= r1 by Th81;
consider r2 being real number such that
A3: for c being Element of C st c in Y /\ (dom f2) holds
|.(f2 /. c).| <= r2 by A1, Th81;
ex p1 being real number 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 )
assume c in (X /\ Y) /\ (dom (f1 + f2)) ; :: thesis: |.((f1 + f2) /. c).| <= r0
then A4: ( c in X /\ Y & c in dom (f1 + f2) ) by XBOOLE_0:def 4;
then ( c in X & c in Y & c in (dom f1) /\ (dom f2) ) by VALUED_1:def 1, XBOOLE_0:def 4;
then ( c in X & c in Y & c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
then A5: ( c in X /\ (dom f1) & c in Y /\ (dom f2) ) by XBOOLE_0:def 4;
then A6: |.(f1 /. c).| <= r1 by A2;
|.(f2 /. c).| <= r2 by A3, A5;
then A7: |.(f1 /. c).| + |.(f2 /. c).| <= r0 by A6, XREAL_1:9;
|.((f1 /. c) + (f2 /. c)).| <= |.(f1 /. c).| + |.(f2 /. c).| by COMPLEX1:142;
then |.((f1 /. c) + (f2 /. c)).| <= r0 by A7, XXREAL_0:2;
hence |.((f1 + f2) /. c).| <= r0 by A4, Th3; :: thesis: verum

end;

hence (f1 + f2) | (X /\ Y) is bounded by Th81; :: thesis: verum