let X be non empty set ; for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for F being Function of RAT ,S
for r being Real
for A being Element of S st f is real-valued & g is real-valued & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let S be SigmaField of X; for f, g being PartFunc of X,ExtREAL
for F being Function of RAT ,S
for r being Real
for A being Element of S st f is real-valued & g is real-valued & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let f, g be PartFunc of X,ExtREAL ; for F being Function of RAT ,S
for r being Real
for A being Element of S st f is real-valued & g is real-valued & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let F be Function of RAT ,S; for r being Real
for A being Element of S st f is real-valued & g is real-valued & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let r be Real; for A being Element of S st f is real-valued & g is real-valued & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let A be Element of S; ( f is real-valued & g is real-valued & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) implies A /\ (less_dom (f + g),(R_EAL r)) = union (rng F) )
assume that
A1:
f is real-valued
and
A2:
g is real-valued
and
A3:
for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
; A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
A4:
dom (f + g) = (dom f) /\ (dom g)
by A1, Th2;
A5:
A /\ (less_dom (f + g),(R_EAL r)) c= union (rng F)
proof
let x be
set ;
TARSKI:def 3 ( not x in A /\ (less_dom (f + g),(R_EAL r)) or x in union (rng F) )
assume A6:
x in A /\ (less_dom (f + g),(R_EAL r))
;
x in union (rng F)
A7:
x in A
by A6, XBOOLE_0:def 4;
A8:
x in less_dom (f + g),
(R_EAL r)
by A6, XBOOLE_0:def 4;
A9:
x in dom (f + g)
by A8, MESFUNC1:def 12;
A10:
(f + g) . x < R_EAL r
by A8, MESFUNC1:def 12;
reconsider x =
x as
Element of
X by A6;
A11:
(f . x) + (g . x) < R_EAL r
by A9, A10, MESFUNC1:def 3;
A12:
x in dom f
by A4, A9, XBOOLE_0:def 4;
A13:
x in dom g
by A4, A9, XBOOLE_0:def 4;
A14:
|.(f . x).| < +infty
by A1, A12, Def1;
A15:
|.(g . x).| < +infty
by A2, A13, Def1;
A16:
- +infty < f . x
by A14, EXTREAL2:58;
A17:
f . x < +infty
by A14, EXTREAL2:58;
A18:
- +infty < g . x
by A15, EXTREAL2:58;
A19:
g . x < +infty
by A15, EXTREAL2:58;
A20:
f . x < (R_EAL r) - (g . x)
by A11, A17, A19, XXREAL_3:63;
A21:
-infty < f . x
by A16, XXREAL_3:23;
A22:
-infty < g . x
by A18, XXREAL_3:23;
reconsider f1 =
f . x as
Real by A17, A21, XXREAL_0:14;
reconsider g1 =
g . x as
Real by A19, A22, XXREAL_0:14;
A23:
(R_EAL r) - (g . x) = r - g1
by SUPINF_2:5;
consider p being
Rational such that A24:
f1 < p
and A25:
p < r - g1
by A20, A23, RAT_1:22;
A26:
not
r - p <= g1
by A25, XREAL_1:14;
A27:
x in less_dom f,
(R_EAL p)
by A12, A24, MESFUNC1:def 12;
A28:
x in less_dom g,
(R_EAL (r - p))
by A13, A26, MESFUNC1:def 12;
A29:
x in A /\ (less_dom f,(R_EAL p))
by A7, A27, XBOOLE_0:def 4;
A30:
x in A /\ (less_dom g,(R_EAL (r - p)))
by A7, A28, XBOOLE_0:def 4;
A31:
x in (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
by A29, A30, XBOOLE_0:def 4;
A32:
p in RAT
by RAT_1:def 2;
A33:
p in dom F
by A32, FUNCT_2:def 1;
A34:
x in F . p
by A3, A31;
A35:
F . p in rng F
by A33, FUNCT_1:def 5;
thus
x in union (rng F)
by A34, A35, TARSKI:def 4;
verum
end;
A36:
union (rng F) c= A /\ (less_dom (f + g),(R_EAL r))
proof
let x be
set ;
TARSKI:def 3 ( not x in union (rng F) or x in A /\ (less_dom (f + g),(R_EAL r)) )
assume A37:
x in union (rng F)
;
x in A /\ (less_dom (f + g),(R_EAL r))
consider Y being
set such that A38:
x in Y
and A39:
Y in rng F
by A37, TARSKI:def 4;
consider p being
set such that A40:
p in dom F
and A41:
Y = F . p
by A39, FUNCT_1:def 5;
reconsider p =
p as
Rational by A40;
A42:
x in (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
by A3, A38, A41;
A43:
x in A /\ (less_dom f,(R_EAL p))
by A42, XBOOLE_0:def 4;
A44:
x in A /\ (less_dom g,(R_EAL (r - p)))
by A42, XBOOLE_0:def 4;
A45:
x in A
by A43, XBOOLE_0:def 4;
A46:
x in less_dom f,
(R_EAL p)
by A43, XBOOLE_0:def 4;
A47:
x in less_dom g,
(R_EAL (r - p))
by A44, XBOOLE_0:def 4;
A48:
x in dom f
by A46, MESFUNC1:def 12;
A49:
x in dom g
by A47, MESFUNC1:def 12;
reconsider x =
x as
Element of
X by A42;
A50:
g . x < R_EAL (r - p)
by A47, MESFUNC1:def 12;
A51:
|.(f . x).| < +infty
by A1, A48, Def1;
A52:
|.(g . x).| < +infty
by A2, A49, Def1;
A53:
- +infty < f . x
by A51, EXTREAL2:58;
A54:
- +infty < g . x
by A52, EXTREAL2:58;
A55:
-infty < f . x
by A53, XXREAL_3:23;
A56:
f . x < +infty
by A51, EXTREAL2:58;
A57:
-infty < g . x
by A54, XXREAL_3:23;
A58:
g . x < +infty
by A52, EXTREAL2:58;
reconsider f1 =
f . x as
Real by A55, A56, XXREAL_0:14;
reconsider g1 =
g . x as
Real by A57, A58, XXREAL_0:14;
A59:
f1 < p
by A46, MESFUNC1:def 12;
A60:
p < r - g1
by A50, XREAL_1:14;
A61:
f1 < r - g1
by A59, A60, XXREAL_0:2;
A62:
f1 + g1 < r
by A61, XREAL_1:22;
A63:
x in dom (f + g)
by A4, A48, A49, XBOOLE_0:def 4;
A64:
(f + g) . x =
(f . x) + (g . x)
by A63, MESFUNC1:def 3
.=
f1 + g1
by SUPINF_2:1
;
A65:
x in less_dom (f + g),
(R_EAL r)
by A62, A63, A64, MESFUNC1:def 12;
thus
x in A /\ (less_dom (f + g),(R_EAL r))
by A45, A65, XBOOLE_0:def 4;
verum
end;
thus
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
by A5, A36, XBOOLE_0:def 10; verum