let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is DFPG -measurable )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is DFPG -measurable )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is DFPG -measurable )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) & dom f = dom g implies ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is DFPG -measurable ) )
assume that
A1: ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) and
A2: ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) and
A3: dom f = dom g ; :: thesis: ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is DFPG -measurable )
consider Gf being Element of S such that
A4: Gf = dom g and
A5: g is Gf -measurable by A2;
now :: thesis: for v being object st v in g " {-infty} holds
v in Gf /\ (eq_dom (g,-infty))
let v be object ; :: thesis: ( v in g " {-infty} implies v in Gf /\ (eq_dom (g,-infty)) )
assume A6: v in g " {-infty} ; :: thesis: v in Gf /\ (eq_dom (g,-infty))
then A7: v in dom g by FUNCT_1:def 7;
g . v in {-infty} by A6, FUNCT_1:def 7;
then g . v = -infty by TARSKI:def 1;
then v in eq_dom (g,-infty) by A7, MESFUNC1:def 15;
hence v in Gf /\ (eq_dom (g,-infty)) by A4, A7, XBOOLE_0:def 4; :: thesis: verum
end;
then A8: g " {-infty} c= Gf /\ (eq_dom (g,-infty)) ;
now :: thesis: for v being object st v in Gf /\ (eq_dom (g,-infty)) holds
v in g " {-infty}
let v be object ; :: thesis: ( v in Gf /\ (eq_dom (g,-infty)) implies v in g " {-infty} )
assume v in Gf /\ (eq_dom (g,-infty)) ; :: thesis: v in g " {-infty}
then A9: v in eq_dom (g,-infty) by XBOOLE_0:def 4;
then g . v = -infty by MESFUNC1:def 15;
then A10: g . v in {-infty} by TARSKI:def 1;
v in dom g by A9, MESFUNC1:def 15;
hence v in g " {-infty} by A10, FUNCT_1:def 7; :: thesis: verum
end;
then A11: Gf /\ (eq_dom (g,-infty)) c= g " {-infty} ;
Gf /\ (eq_dom (g,-infty)) in S by A5, MESFUNC1:34;
then A12: g " {-infty} in S by A8, A11, XBOOLE_0:def 10;
now :: thesis: for v being object st v in g " {+infty} holds
v in Gf /\ (eq_dom (g,+infty))
let v be object ; :: thesis: ( v in g " {+infty} implies v in Gf /\ (eq_dom (g,+infty)) )
assume A13: v in g " {+infty} ; :: thesis: v in Gf /\ (eq_dom (g,+infty))
then A14: v in dom g by FUNCT_1:def 7;
g . v in {+infty} by A13, FUNCT_1:def 7;
then g . v = +infty by TARSKI:def 1;
then v in eq_dom (g,+infty) by A14, MESFUNC1:def 15;
hence v in Gf /\ (eq_dom (g,+infty)) by A4, A14, XBOOLE_0:def 4; :: thesis: verum
end;
then A15: g " {+infty} c= Gf /\ (eq_dom (g,+infty)) ;
now :: thesis: for v being object st v in Gf /\ (eq_dom (g,+infty)) holds
v in g " {+infty}
let v be object ; :: thesis: ( v in Gf /\ (eq_dom (g,+infty)) implies v in g " {+infty} )
assume v in Gf /\ (eq_dom (g,+infty)) ; :: thesis: v in g " {+infty}
then A16: v in eq_dom (g,+infty) by XBOOLE_0:def 4;
then g . v = +infty by MESFUNC1:def 15;
then A17: g . v in {+infty} by TARSKI:def 1;
v in dom g by A16, MESFUNC1:def 15;
hence v in g " {+infty} by A17, FUNCT_1:def 7; :: thesis: verum
end;
then A18: Gf /\ (eq_dom (g,+infty)) c= g " {+infty} ;
A19: (f " {+infty}) /\ (g " {-infty}) c= g " {-infty} by XBOOLE_1:17;
A20: (f " {-infty}) /\ (g " {+infty}) c= f " {-infty} by XBOOLE_1:17;
A21: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;
Gf /\ (eq_dom (g,+infty)) in S by A4, A5, MESFUNC1:33;
then A22: g " {+infty} in S by A15, A18, XBOOLE_0:def 10;
then reconsider NG = (g " {+infty}) \/ (g " {-infty}) as Element of S by A12, PROB_1:3;
consider E0 being Element of S such that
A23: E0 = dom f and
A24: f is E0 -measurable by A1;
A25: E0 /\ (eq_dom (f,+infty)) in S by A23, A24, MESFUNC1:33;
now :: thesis: for v being object st v in E0 /\ (eq_dom (f,+infty)) holds
v in f " {+infty}
let v be object ; :: thesis: ( v in E0 /\ (eq_dom (f,+infty)) implies v in f " {+infty} )
assume v in E0 /\ (eq_dom (f,+infty)) ; :: thesis: v in f " {+infty}
then A26: v in eq_dom (f,+infty) by XBOOLE_0:def 4;
then f . v = +infty by MESFUNC1:def 15;
then A27: f . v in {+infty} by TARSKI:def 1;
v in dom f by A26, MESFUNC1:def 15;
hence v in f " {+infty} by A27, FUNCT_1:def 7; :: thesis: verum
end;
then A28: E0 /\ (eq_dom (f,+infty)) c= f " {+infty} ;
now :: thesis: for v being object st v in f " {+infty} holds
v in E0 /\ (eq_dom (f,+infty))
let v be object ; :: thesis: ( v in f " {+infty} implies v in E0 /\ (eq_dom (f,+infty)) )
assume A29: v in f " {+infty} ; :: thesis: v in E0 /\ (eq_dom (f,+infty))
then A30: v in dom f by FUNCT_1:def 7;
f . v in {+infty} by A29, FUNCT_1:def 7;
then f . v = +infty by TARSKI:def 1;
then v in eq_dom (f,+infty) by A30, MESFUNC1:def 15;
hence v in E0 /\ (eq_dom (f,+infty)) by A23, A30, XBOOLE_0:def 4; :: thesis: verum
end;
then f " {+infty} c= E0 /\ (eq_dom (f,+infty)) ;
then A31: f " {+infty} = E0 /\ (eq_dom (f,+infty)) by A28;
now :: thesis: for v being object st v in E0 /\ (eq_dom (f,-infty)) holds
v in f " {-infty}
let v be object ; :: thesis: ( v in E0 /\ (eq_dom (f,-infty)) implies v in f " {-infty} )
assume v in E0 /\ (eq_dom (f,-infty)) ; :: thesis: v in f " {-infty}
then A32: v in eq_dom (f,-infty) by XBOOLE_0:def 4;
then f . v = -infty by MESFUNC1:def 15;
then A33: f . v in {-infty} by TARSKI:def 1;
v in dom f by A32, MESFUNC1:def 15;
hence v in f " {-infty} by A33, FUNCT_1:def 7; :: thesis: verum
end;
then A34: E0 /\ (eq_dom (f,-infty)) c= f " {-infty} ;
now :: thesis: for v being object st v in f " {-infty} holds
v in E0 /\ (eq_dom (f,-infty))
let v be object ; :: thesis: ( v in f " {-infty} implies v in E0 /\ (eq_dom (f,-infty)) )
assume A35: v in f " {-infty} ; :: thesis: v in E0 /\ (eq_dom (f,-infty))
then A36: v in dom f by FUNCT_1:def 7;
f . v in {-infty} by A35, FUNCT_1:def 7;
then f . v = -infty by TARSKI:def 1;
then v in eq_dom (f,-infty) by A36, MESFUNC1:def 15;
hence v in E0 /\ (eq_dom (f,-infty)) by A23, A36, XBOOLE_0:def 4; :: thesis: verum
end;
then A37: f " {-infty} c= E0 /\ (eq_dom (f,-infty)) ;
then A38: f " {-infty} = E0 /\ (eq_dom (f,-infty)) by A34;
A39: E0 /\ (eq_dom (f,-infty)) in S by A24, MESFUNC1:34;
then A40: f " {-infty} in S by A37, A34, XBOOLE_0:def 10;
then reconsider NF = (f " {+infty}) \/ (f " {-infty}) as Element of S by A25, A31, PROB_1:3;
reconsider NFG = NF \/ NG as Element of S ;
reconsider E = E0 \ NFG as Element of S ;
reconsider DFPG = dom (f + g) as Element of S by A1, A2, A25, A31, A40, A22, A12, Th46;
set g1 = g | E;
set f1 = f | E;
A41: (dom f) /\ E = E by A23, XBOOLE_1:28, XBOOLE_1:36;
g " {-infty} c= NG by XBOOLE_1:7;
then A42: (f " {+infty}) /\ (g " {-infty}) c= NG by A19;
f " {-infty} c= NF by XBOOLE_1:7;
then (f " {-infty}) /\ (g " {+infty}) c= NF by A20;
then ((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})) c= NF \/ NG by A42, XBOOLE_1:13;
then A43: E c= dom (f + g) by A3, A23, A21, XBOOLE_1:34;
then A44: (f + g) | E = (f | E) + (g | E) by Th29;
A45: dom ((f | E) + (g | E)) = E by A43, Th29;
A46: E = dom ((f | E) + (g | E)) by A43, Th29;
A47: for r being Real holds DFPG /\ (less_dom ((f + g),r)) = ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
proof
let r be Real; :: thesis: DFPG /\ (less_dom ((f + g),r)) = ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
set SL = DFPG /\ (less_dom ((f + g),r));
set SR = ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})));
A48: now :: thesis: for x being object st x in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) holds
x in DFPG /\ (less_dom ((f + g),r))
let x be object ; :: thesis: ( x in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) implies b1 in DFPG /\ (less_dom ((f + g),r)) )
reconsider xx = x as set by TARSKI:1;
assume x in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) ; :: thesis: b1 in DFPG /\ (less_dom ((f + g),r))
then A49: ( x in (E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty}))) or x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) ) by XBOOLE_0:def 3;
per cases ( x in E /\ (less_dom (((f | E) + (g | E)),r)) or x in (f " {-infty}) /\ (DFPG \ (g " {+infty})) or x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) ) by A49, XBOOLE_0:def 3;
suppose A50: x in E /\ (less_dom (((f | E) + (g | E)),r)) ; :: thesis: b1 in DFPG /\ (less_dom ((f + g),r))
then A51: x in E by XBOOLE_0:def 4;
x in less_dom (((f | E) + (g | E)),r) by A50, XBOOLE_0:def 4;
then ((f | E) + (g | E)) . xx < r by MESFUNC1:def 11;
then (f + g) . xx < r by A44, A45, A51, FUNCT_1:47;
then x in less_dom ((f + g),r) by A43, A51, MESFUNC1:def 11;
hence x in DFPG /\ (less_dom ((f + g),r)) by A43, A51, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A52: ( x in (f " {-infty}) /\ (DFPG \ (g " {+infty})) or x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) ) ; :: thesis: b1 in DFPG /\ (less_dom ((f + g),r))
per cases ( x in (f " {-infty}) /\ (DFPG \ (g " {+infty})) or x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) ) by A52;
suppose A53: x in (f " {-infty}) /\ (DFPG \ (g " {+infty})) ; :: thesis: b1 in DFPG /\ (less_dom ((f + g),r))
r in REAL by XREAL_0:def 1;
then A54: -infty < r by XXREAL_0:12;
A55: x in DFPG \ (g " {+infty}) by A53, XBOOLE_0:def 4;
then A56: x in DFPG by XBOOLE_0:def 5;
then x in ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;
then A57: x in (dom f) /\ (dom g) by XBOOLE_0:def 5;
then x in dom g by XBOOLE_0:def 4;
then ( x in g " {+infty} iff g . x in {+infty} ) by FUNCT_1:def 7;
then A58: ( x in g " {+infty} iff g . x = +infty ) by TARSKI:def 1;
x in dom f by A57, XBOOLE_0:def 4;
then ( x in f " {-infty} iff f . x in {-infty} ) by FUNCT_1:def 7;
then ( x in f " {-infty} iff f . x = -infty ) by TARSKI:def 1;
then (f . xx) + (g . xx) = -infty by A53, A55, A58, XBOOLE_0:def 4, XBOOLE_0:def 5, XXREAL_3:def 2;
then (f + g) . xx < r by A56, A54, MESFUNC1:def 3;
then x in less_dom ((f + g),r) by A56, MESFUNC1:def 11;
hence x in DFPG /\ (less_dom ((f + g),r)) by A56, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A59: x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) ; :: thesis: b1 in DFPG /\ (less_dom ((f + g),r))
r in REAL by XREAL_0:def 1;
then A60: -infty < r by XXREAL_0:12;
A61: x in DFPG \ (f " {+infty}) by A59, XBOOLE_0:def 4;
then A62: x in DFPG by XBOOLE_0:def 5;
A63: x in DFPG by A61, XBOOLE_0:def 5;
then x in ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;
then A64: x in (dom f) /\ (dom g) by XBOOLE_0:def 5;
then x in dom g by XBOOLE_0:def 4;
then ( x in g " {-infty} iff g . x in {-infty} ) by FUNCT_1:def 7;
then A65: ( x in g " {-infty} iff g . x = -infty ) by TARSKI:def 1;
x in dom f by A64, XBOOLE_0:def 4;
then ( x in f " {+infty} iff f . x in {+infty} ) by FUNCT_1:def 7;
then ( x in f " {+infty} iff f . x = +infty ) by TARSKI:def 1;
then (f . xx) + (g . xx) = -infty by A59, A61, A65, XBOOLE_0:def 4, XBOOLE_0:def 5, XXREAL_3:def 2;
then (f + g) . xx < r by A62, A60, MESFUNC1:def 3;
then x in less_dom ((f + g),r) by A62, MESFUNC1:def 11;
hence x in DFPG /\ (less_dom ((f + g),r)) by A63, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
end;
end;
now :: thesis: for x being object st x in DFPG /\ (less_dom ((f + g),r)) holds
x in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
let x be object ; :: thesis: ( x in DFPG /\ (less_dom ((f + g),r)) implies b1 in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) )
reconsider xx = x as set by TARSKI:1;
assume A66: x in DFPG /\ (less_dom ((f + g),r)) ; :: thesis: b1 in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
then A67: x in DFPG by XBOOLE_0:def 4;
then A68: x in ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;
then A69: not x in ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) by XBOOLE_0:def 5;
then A70: not x in (f " {+infty}) /\ (g " {-infty}) by XBOOLE_0:def 3;
x in less_dom ((f + g),r) by A66, XBOOLE_0:def 4;
then A71: (f + g) . xx < r by MESFUNC1:def 11;
then A72: (f . xx) + (g . xx) < r by A67, MESFUNC1:def 3;
A73: not x in (f " {-infty}) /\ (g " {+infty}) by A69, XBOOLE_0:def 3;
A74: x in (dom f) /\ (dom g) by A68, XBOOLE_0:def 5;
then A75: x in dom f by XBOOLE_0:def 4;
then A76: ( x in f " {-infty} iff f . x in {-infty} ) by FUNCT_1:def 7;
A77: ( x in f " {+infty} iff f . x in {+infty} ) by A75, FUNCT_1:def 7;
then A78: ( x in f " {+infty} iff f . x = +infty ) by TARSKI:def 1;
A79: x in dom g by A74, XBOOLE_0:def 4;
then A80: ( x in g " {-infty} iff g . x in {-infty} ) by FUNCT_1:def 7;
A81: ( x in g " {+infty} iff g . x in {+infty} ) by A79, FUNCT_1:def 7;
then A82: ( x in g " {+infty} iff g . x = +infty ) by TARSKI:def 1;
per cases ( f . x = -infty or f . x <> -infty ) ;
suppose A83: f . x = -infty ; :: thesis: b1 in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
then x in DFPG \ (g " {+infty}) by A67, A76, A81, A73, TARSKI:def 1, XBOOLE_0:def 4, XBOOLE_0:def 5;
then x in (f " {-infty}) /\ (DFPG \ (g " {+infty})) by A76, A83, TARSKI:def 1, XBOOLE_0:def 4;
then x in (E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty}))) by XBOOLE_0:def 3;
hence x in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A84: f . x <> -infty ; :: thesis: b1 in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
per cases ( g . x = -infty or g . x <> -infty ) ;
suppose A85: g . x = -infty ; :: thesis: b1 in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
then x in DFPG \ (f " {+infty}) by A67, A77, A80, A70, TARSKI:def 1, XBOOLE_0:def 4, XBOOLE_0:def 5;
then x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) by A80, A85, TARSKI:def 1, XBOOLE_0:def 4;
hence x in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A86: g . x <> -infty ; :: thesis: b1 in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))
then not x in (f " {-infty}) \/ (f " {+infty}) by A76, A78, A72, A84, TARSKI:def 1, XBOOLE_0:def 3, XXREAL_3:52;
then not x in ((f " {-infty}) \/ (f " {+infty})) \/ (g " {-infty}) by A80, A86, TARSKI:def 1, XBOOLE_0:def 3;
then not x in (((f " {-infty}) \/ (f " {+infty})) \/ (g " {-infty})) \/ (g " {+infty}) by A82, A72, A84, XBOOLE_0:def 3, XXREAL_3:52;
then not x in NFG by XBOOLE_1:4;
then A87: x in E by A23, A75, XBOOLE_0:def 5;
then ((f | E) + (g | E)) . x = (f + g) . x by A44, A45, FUNCT_1:47;
then x in less_dom (((f | E) + (g | E)),r) by A46, A71, A87, MESFUNC1:def 11;
then x in E /\ (less_dom (((f | E) + (g | E)),r)) by A87, XBOOLE_0:def 4;
then x in (E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty}))) by XBOOLE_0:def 3;
hence x in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
end;
end;
hence DFPG /\ (less_dom ((f + g),r)) = ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) by A48, TARSKI:2; :: thesis: verum
end;
A88: now :: thesis: for x being set st x in dom (f | E) holds
( -infty < (f | E) . x & (f | E) . x < +infty )
let x be set ; :: thesis: ( x in dom (f | E) implies ( -infty < (f | E) . x & (f | E) . x < +infty ) )
for x being object st x in dom f holds
f . x in ExtREAL by XXREAL_0:def 1;
then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:3;
assume A89: x in dom (f | E) ; :: thesis: ( -infty < (f | E) . x & (f | E) . x < +infty )
then A90: x in (dom f) /\ E by RELAT_1:61;
then A91: x in dom f by XBOOLE_0:def 4;
x in E by A90, XBOOLE_0:def 4;
then A92: not x in NFG by XBOOLE_0:def 5;
A93: now :: thesis: not (f | E) . x = -infty
assume (f | E) . x = -infty ; :: thesis: contradiction
then f . x = -infty by A89, FUNCT_1:47;
then ff . x in {-infty} by TARSKI:def 1;
then A94: x in ff " {-infty} by A91, FUNCT_2:38;
f " {-infty} c= NF by XBOOLE_1:7;
hence contradiction by A92, A94, XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: not (f | E) . x = +infty
assume (f | E) . x = +infty ; :: thesis: contradiction
then f . x = +infty by A89, FUNCT_1:47;
then f . x in {+infty} by TARSKI:def 1;
then A95: x in ff " {+infty} by A91, FUNCT_2:38;
f " {+infty} c= NF by XBOOLE_1:7;
hence contradiction by A92, A95, XBOOLE_0:def 3; :: thesis: verum
end;
hence ( -infty < (f | E) . x & (f | E) . x < +infty ) by A93, XXREAL_0:4, XXREAL_0:6; :: thesis: verum
end;
now :: thesis: for x being Element of X st x in dom (f | E) holds
|.((f | E) . x).| < +infty
let x be Element of X; :: thesis: ( x in dom (f | E) implies |.((f | E) . x).| < +infty )
A96: - +infty = -infty by XXREAL_3:def 3;
assume A97: x in dom (f | E) ; :: thesis: |.((f | E) . x).| < +infty
then A98: (f | E) . x < +infty by A88;
-infty < (f | E) . x by A88, A97;
hence |.((f | E) . x).| < +infty by A98, A96, EXTREAL1:22; :: thesis: verum
end;
then A99: f | E is real-valued by MESFUNC2:def 1;
A100: now :: thesis: for x being set st x in dom (g | E) holds
( -infty < (g | E) . x & (g | E) . x < +infty )
let x be set ; :: thesis: ( x in dom (g | E) implies ( -infty < (g | E) . x & (g | E) . x < +infty ) )
for x being object st x in dom g holds
g . x in ExtREAL by XXREAL_0:def 1;
then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:3;
assume A101: x in dom (g | E) ; :: thesis: ( -infty < (g | E) . x & (g | E) . x < +infty )
then A102: x in (dom g) /\ E by RELAT_1:61;
then A103: x in dom g by XBOOLE_0:def 4;
x in E by A102, XBOOLE_0:def 4;
then A104: not x in NFG by XBOOLE_0:def 5;
A105: now :: thesis: not (g | E) . x = -infty
assume (g | E) . x = -infty ; :: thesis: contradiction
then g . x = -infty by A101, FUNCT_1:47;
then gg . x in {-infty} by TARSKI:def 1;
then A106: x in gg " {-infty} by A103, FUNCT_2:38;
g " {-infty} c= NG by XBOOLE_1:7;
hence contradiction by A104, A106, XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: not (g | E) . x = +infty
assume (g | E) . x = +infty ; :: thesis: contradiction
then g . x = +infty by A101, FUNCT_1:47;
then gg . x in {+infty} by TARSKI:def 1;
then A107: x in gg " {+infty} by A103, FUNCT_2:38;
g " {+infty} c= NG by XBOOLE_1:7;
hence contradiction by A104, A107, XBOOLE_0:def 3; :: thesis: verum
end;
hence ( -infty < (g | E) . x & (g | E) . x < +infty ) by A105, XXREAL_0:4, XXREAL_0:6; :: thesis: verum
end;
now :: thesis: for x being Element of X st x in dom (g | E) holds
|.((g | E) . x).| < +infty
let x be Element of X; :: thesis: ( x in dom (g | E) implies |.((g | E) . x).| < +infty )
A108: - +infty = -infty by XXREAL_3:def 3;
assume A109: x in dom (g | E) ; :: thesis: |.((g | E) . x).| < +infty
then A110: (g | E) . x < +infty by A100;
-infty < (g | E) . x by A100, A109;
hence |.((g | E) . x).| < +infty by A110, A108, EXTREAL1:22; :: thesis: verum
end;
then A111: g | E is real-valued by MESFUNC2:def 1;
f is E -measurable by A1, A23, MESFUNC1:30, XBOOLE_1:36;
then A112: f | E is E -measurable by A41, Th42;
A113: (dom g) /\ E = E by A3, A23, XBOOLE_1:28, XBOOLE_1:36;
g is E -measurable by A2, A3, A23, MESFUNC1:30, XBOOLE_1:36;
then g | E is E -measurable by A113, Th42;
then A114: (f | E) + (g | E) is E -measurable by A112, A99, A111, MESFUNC2:7;
now :: thesis: for r being Real holds DFPG /\ (less_dom ((f + g),r)) in S
let r be Real; :: thesis: DFPG /\ (less_dom ((f + g),r)) in S
A115: E /\ (less_dom (((f | E) + (g | E)),r)) in S by A114, MESFUNC1:def 16;
DFPG \ (f " {+infty}) in S by A25, A31, PROB_1:6;
then A116: (g " {-infty}) /\ (DFPG \ (f " {+infty})) in S by A12, FINSUB_1:def 2;
DFPG \ (g " {+infty}) in S by A22, PROB_1:6;
then (f " {-infty}) /\ (DFPG \ (g " {+infty})) in S by A39, A38, FINSUB_1:def 2;
then ((f " {-infty}) /\ (DFPG \ (g " {+infty}))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) in S by A116, PROB_1:3;
then A117: (E /\ (less_dom (((f | E) + (g | E)),r))) \/ (((f " {-infty}) /\ (DFPG \ (g " {+infty}))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))) in S by A115, PROB_1:3;
DFPG /\ (less_dom ((f + g),r)) = ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty}))) by A47;
hence DFPG /\ (less_dom ((f + g),r)) in S by A117, XBOOLE_1:4; :: thesis: verum
end;
then f + g is DFPG -measurable by MESFUNC1:def 16;
hence ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is DFPG -measurable ) ; :: thesis: verum