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 V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),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 V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),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 V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let F be Function of RAT,S; for r being Real
for A being Element of S st f is V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let r be Real; for A being Element of S st f is V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
let A be Element of S; ( f is V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) implies A /\ (less_dom ((f + g),r)) = union (rng F) )
assume that
A1:
f is V82()
and
A2:
g is V82()
and
A3:
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
; A /\ (less_dom ((f + g),r)) = union (rng F)
A4:
dom (f + g) = (dom f) /\ (dom g)
by A1, Th2;
A5:
A /\ (less_dom ((f + g),r)) c= union (rng F)
proof
let x be
object ;
TARSKI:def 3 ( not x in A /\ (less_dom ((f + g),r)) or x in union (rng F) )
assume A6:
x in A /\ (less_dom ((f + g),r))
;
x in union (rng F)
then A7:
x in A
by XBOOLE_0:def 4;
A8:
x in less_dom (
(f + g),
r)
by A6, XBOOLE_0:def 4;
then A9:
x in dom (f + g)
by MESFUNC1:def 11;
A10:
(f + g) . x < r
by A8, MESFUNC1:def 11;
reconsider x =
x as
Element of
X by A6;
A11:
(f . x) + (g . x) < 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;
A15:
|.(g . x).| < +infty
by A2, A13;
A16:
- +infty < f . x
by A14, EXTREAL1:21;
A17:
f . x < +infty
by A14, EXTREAL1:21;
A18:
- +infty < g . x
by A15, EXTREAL1:21;
A19:
g . x < +infty
by A15, EXTREAL1:21;
then A20:
f . x < r - (g . x)
by A11, A17, XXREAL_3:52;
A21:
-infty < f . x
by A16, XXREAL_3:23;
A22:
-infty < g . x
by A18, XXREAL_3:23;
reconsider f1 =
f . x as
Element of
REAL by A17, A21, XXREAL_0:14;
reconsider g1 =
g . x as
Element of
REAL by A19, A22, XXREAL_0:14;
reconsider rr =
r as
R_eal by XXREAL_0:def 1;
f1 < r - g1
by A20, SUPINF_2:3;
then consider p being
Rational such that A23:
f1 < p
and A24:
p < r - g1
by RAT_1:7;
A25:
not
r - p <= g1
by A24, XREAL_1:12;
A26:
x in less_dom (
f,
p)
by A12, A23, MESFUNC1:def 11;
A27:
x in less_dom (
g,
(r - p))
by A13, A25, MESFUNC1:def 11;
A28:
x in A /\ (less_dom (f,p))
by A7, A26, XBOOLE_0:def 4;
x in A /\ (less_dom (g,(r - p)))
by A7, A27, XBOOLE_0:def 4;
then A29:
x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
by A28, XBOOLE_0:def 4;
p in RAT
by RAT_1:def 2;
then A30:
p in dom F
by FUNCT_2:def 1;
A31:
x in F . p
by A3, A29;
F . p in rng F
by A30, FUNCT_1:def 3;
hence
x in union (rng F)
by A31, TARSKI:def 4;
verum
end;
union (rng F) c= A /\ (less_dom ((f + g),r))
proof
let x be
object ;
TARSKI:def 3 ( not x in union (rng F) or x in A /\ (less_dom ((f + g),r)) )
assume
x in union (rng F)
;
x in A /\ (less_dom ((f + g),r))
then consider Y being
set such that A32:
x in Y
and A33:
Y in rng F
by TARSKI:def 4;
consider p being
object such that A34:
p in dom F
and A35:
Y = F . p
by A33, FUNCT_1:def 3;
reconsider p =
p as
Rational by A34;
A36:
x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
by A3, A32, A35;
then A37:
x in A /\ (less_dom (f,p))
by XBOOLE_0:def 4;
A38:
x in A /\ (less_dom (g,(r - p)))
by A36, XBOOLE_0:def 4;
A39:
x in A
by A37, XBOOLE_0:def 4;
A40:
x in less_dom (
f,
p)
by A37, XBOOLE_0:def 4;
A41:
x in less_dom (
g,
(r - p))
by A38, XBOOLE_0:def 4;
A42:
x in dom f
by A40, MESFUNC1:def 11;
A43:
x in dom g
by A41, MESFUNC1:def 11;
reconsider x =
x as
Element of
X by A36;
A44:
g . x < r - p
by A41, MESFUNC1:def 11;
A45:
|.(f . x).| < +infty
by A1, A42;
A46:
|.(g . x).| < +infty
by A2, A43;
A47:
- +infty < f . x
by A45, EXTREAL1:21;
A48:
- +infty < g . x
by A46, EXTREAL1:21;
A49:
-infty < f . x
by A47, XXREAL_3:23;
A50:
f . x < +infty
by A45, EXTREAL1:21;
A51:
-infty < g . x
by A48, XXREAL_3:23;
A52:
g . x < +infty
by A46, EXTREAL1:21;
reconsider f1 =
f . x as
Element of
REAL by A49, A50, XXREAL_0:14;
reconsider g1 =
g . x as
Element of
REAL by A51, A52, XXREAL_0:14;
A53:
f1 < p
by A40, MESFUNC1:def 11;
p < r - g1
by A44, XREAL_1:12;
then
f1 < r - g1
by A53, XXREAL_0:2;
then A54:
f1 + g1 < r
by XREAL_1:20;
A55:
x in dom (f + g)
by A4, A42, A43, XBOOLE_0:def 4;
then (f + g) . x =
(f . x) + (g . x)
by MESFUNC1:def 3
.=
f1 + g1
by SUPINF_2:1
;
then
x in less_dom (
(f + g),
r)
by A54, A55, MESFUNC1:def 11;
hence
x in A /\ (less_dom ((f + g),r))
by A39, XBOOLE_0:def 4;
verum
end;
hence
A /\ (less_dom ((f + g),r)) = union (rng F)
by A5; verum