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_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG )
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_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG )
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_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) & dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG )
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) & ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) & dom f = dom g implies ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG ) )
assume that
A1: ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) and
A2: ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) and
A3: dom f = dom g ; :: thesis: ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG )
consider Gf being Element of S such that
A4: Gf = dom g and
A5: g is_measurable_on Gf by A2;
now
let v be set ; :: 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 13;
g . v in {-infty } by A6, FUNCT_1:def 13;
then g . v = -infty by TARSKI:def 1;
then v in eq_dom g,-infty by A7, MESFUNC1:def 16;
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 ) by TARSKI:def 3;
now
let v be set ; :: 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 16;
then A10: g . v in {-infty } by TARSKI:def 1;
v in dom g by A9, MESFUNC1:def 16;
hence v in g " {-infty } by A10, FUNCT_1:def 13; :: thesis: verum
end;
then A11: Gf /\ (eq_dom g,-infty ) c= g " {-infty } by TARSKI:def 3;
Gf /\ (eq_dom g,-infty ) in S by A5, MESFUNC1:38;
then A12: g " {-infty } in S by A8, A11, XBOOLE_0:def 10;
now
let v be set ; :: 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 13;
g . v in {+infty } by A13, FUNCT_1:def 13;
then g . v = +infty by TARSKI:def 1;
then v in eq_dom g,+infty by A14, MESFUNC1:def 16;
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 ) by TARSKI:def 3;
now
let v be set ; :: 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 16;
then A17: g . v in {+infty } by TARSKI:def 1;
v in dom g by A16, MESFUNC1:def 16;
hence v in g " {+infty } by A17, FUNCT_1:def 13; :: thesis: verum
end;
then A18: Gf /\ (eq_dom g,+infty ) c= g " {+infty } by TARSKI:def 3;
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:37;
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:9;
consider E0 being Element of S such that
A23: E0 = dom f and
A24: f is_measurable_on E0 by A1;
A25: E0 /\ (eq_dom f,+infty ) in S by A23, A24, MESFUNC1:37;
now
let v be set ; :: 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 16;
then A27: f . v in {+infty } by TARSKI:def 1;
v in dom f by A26, MESFUNC1:def 16;
hence v in f " {+infty } by A27, FUNCT_1:def 13; :: thesis: verum
end;
then A28: E0 /\ (eq_dom f,+infty ) c= f " {+infty } by TARSKI:def 3;
now
let v be set ; :: 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 13;
f . v in {+infty } by A29, FUNCT_1:def 13;
then f . v = +infty by TARSKI:def 1;
then v in eq_dom f,+infty by A30, MESFUNC1:def 16;
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 ) by TARSKI:def 3;
then A31: f " {+infty } = E0 /\ (eq_dom f,+infty ) by A28, XBOOLE_0:def 10;
now
let v be set ; :: 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 16;
then A33: f . v in {-infty } by TARSKI:def 1;
v in dom f by A32, MESFUNC1:def 16;
hence v in f " {-infty } by A33, FUNCT_1:def 13; :: thesis: verum
end;
then A34: E0 /\ (eq_dom f,-infty ) c= f " {-infty } by TARSKI:def 3;
now
let v be set ; :: 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 13;
f . v in {-infty } by A35, FUNCT_1:def 13;
then f . v = -infty by TARSKI:def 1;
then v in eq_dom f,-infty by A36, MESFUNC1:def 16;
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 ) by TARSKI:def 3;
then A38: f " {-infty } = E0 /\ (eq_dom f,-infty ) by A34, XBOOLE_0:def 10;
A39: E0 /\ (eq_dom f,-infty ) in S by A24, MESFUNC1:38;
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:9;
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, Th52;
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, XBOOLE_1:1;
f " {-infty } c= NF by XBOOLE_1:7;
then (f " {-infty }) /\ (g " {+infty }) c= NF by A20, XBOOLE_1:1;
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 Th35;
A45: dom ((f | E) + (g | E)) = E by A43, Th35;
A46: E = dom ((f | E) + (g | E)) by A43, Th35;
A47: for r being real number holds DFPG /\ (less_dom (f + g),(R_EAL r)) = ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })))
proof
let r be real number ; :: thesis: DFPG /\ (less_dom (f + g),(R_EAL r)) = ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })))
set SL = DFPG /\ (less_dom (f + g),(R_EAL r));
set SR = ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })));
A48: now
let x be set ; :: thesis: ( x in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty }))) implies b1 in DFPG /\ (less_dom (f + g),(R_EAL r)) )
assume x in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty }))) ; :: thesis: b1 in DFPG /\ (less_dom (f + g),(R_EAL r))
then A49: ( x in (E /\ (less_dom ((f | E) + (g | E)),(R_EAL 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_EAL 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_EAL r)) ; :: thesis: b1 in DFPG /\ (less_dom (f + g),(R_EAL r))
then A51: x in E by XBOOLE_0:def 4;
x in less_dom ((f | E) + (g | E)),(R_EAL r) by A50, XBOOLE_0:def 4;
then ((f | E) + (g | E)) . x < R_EAL r by MESFUNC1:def 12;
then (f + g) . x < R_EAL r by A44, A45, A51, FUNCT_1:70;
then x in less_dom (f + g),(R_EAL r) by A43, A51, MESFUNC1:def 12;
hence x in DFPG /\ (less_dom (f + g),(R_EAL 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_EAL 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_EAL r))
R_EAL r in REAL by XREAL_0:def 1;
then A54: -infty < R_EAL 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 13;
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 13;
then ( x in f " {-infty } iff f . x = -infty ) by TARSKI:def 1;
then (f . x) + (g . x) = -infty by A53, A55, A58, XBOOLE_0:def 4, XBOOLE_0:def 5, XXREAL_3:def 2;
then (f + g) . x < R_EAL r by A56, A54, MESFUNC1:def 3;
then x in less_dom (f + g),(R_EAL r) by A56, MESFUNC1:def 12;
hence x in DFPG /\ (less_dom (f + g),(R_EAL 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_EAL r))
R_EAL r in REAL by XREAL_0:def 1;
then A60: -infty < R_EAL 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 13;
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 13;
then ( x in f " {+infty } iff f . x = +infty ) by TARSKI:def 1;
then (f . x) + (g . x) = -infty by A59, A61, A65, XBOOLE_0:def 4, XBOOLE_0:def 5, XXREAL_3:def 2;
then (f + g) . x < R_EAL r by A62, A60, MESFUNC1:def 3;
then x in less_dom (f + g),(R_EAL r) by A62, MESFUNC1:def 12;
hence x in DFPG /\ (less_dom (f + g),(R_EAL r)) by A63, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
end;
end;
now
let x be set ; :: thesis: ( x in DFPG /\ (less_dom (f + g),(R_EAL r)) implies b1 in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty }))) )
assume A66: x in DFPG /\ (less_dom (f + g),(R_EAL r)) ; :: thesis: b1 in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL 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_EAL r) by A66, XBOOLE_0:def 4;
then A71: (f + g) . x < R_EAL r by MESFUNC1:def 12;
then A72: (f . x) + (g . x) < R_EAL 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 13;
A77: ( x in f " {+infty } iff f . x in {+infty } ) by A75, FUNCT_1:def 13;
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 13;
A81: ( x in g " {+infty } iff g . x in {+infty } ) by A79, FUNCT_1:def 13;
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_EAL 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_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty }))) by XBOOLE_0:def 3;
hence x in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL 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_EAL 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_EAL 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_EAL 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_EAL 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:63;
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:63;
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:70;
then x in less_dom ((f | E) + (g | E)),(R_EAL r) by A46, A71, A87, MESFUNC1:def 12;
then x in E /\ (less_dom ((f | E) + (g | E)),(R_EAL r)) by A87, XBOOLE_0:def 4;
then x in (E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty }))) by XBOOLE_0:def 3;
hence x in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL 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_EAL r)) = ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty }))) by A48, TARSKI:2; :: thesis: verum
end;
A88: now
let x be set ; :: thesis: ( x in dom (f | E) implies ( -infty < (f | E) . x & (f | E) . x < +infty ) )
for x being set st x in dom f holds
f . x in ExtREAL ;
then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:5;
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:90;
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
assume (f | E) . x = -infty ; :: thesis: contradiction
then f . x = -infty by A89, FUNCT_1:70;
then ff . x in {-infty } by TARSKI:def 1;
then A94: x in ff " {-infty } by A91, FUNCT_2:46;
f " {-infty } c= NF by XBOOLE_1:7;
hence contradiction by A92, A94, XBOOLE_0:def 3; :: thesis: verum
end;
now
assume (f | E) . x = +infty ; :: thesis: contradiction
then f . x = +infty by A89, FUNCT_1:70;
then f . x in {+infty } by TARSKI:def 1;
then A95: x in ff " {+infty } by A91, FUNCT_2:46;
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
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, EXTREAL2:59; :: thesis: verum
end;
then A99: f | E is V61() by MESFUNC2:def 1;
A100: now
let x be set ; :: thesis: ( x in dom (g | E) implies ( -infty < (g | E) . x & (g | E) . x < +infty ) )
for x being set st x in dom g holds
g . x in ExtREAL ;
then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:5;
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:90;
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
assume (g | E) . x = -infty ; :: thesis: contradiction
then g . x = -infty by A101, FUNCT_1:70;
then gg . x in {-infty } by TARSKI:def 1;
then A106: x in gg " {-infty } by A103, FUNCT_2:46;
g " {-infty } c= NG by XBOOLE_1:7;
hence contradiction by A104, A106, XBOOLE_0:def 3; :: thesis: verum
end;
now
assume (g | E) . x = +infty ; :: thesis: contradiction
then g . x = +infty by A101, FUNCT_1:70;
then gg . x in {+infty } by TARSKI:def 1;
then A107: x in gg " {+infty } by A103, FUNCT_2:46;
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
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, EXTREAL2:59; :: thesis: verum
end;
then A111: g | E is V61() by MESFUNC2:def 1;
f is_measurable_on E by A1, A23, MESFUNC1:34, XBOOLE_1:36;
then A112: f | E is_measurable_on E by A41, Th48;
A113: (dom g) /\ E = E by A3, A23, XBOOLE_1:28, XBOOLE_1:36;
g is_measurable_on E by A2, A3, A23, MESFUNC1:34, XBOOLE_1:36;
then g | E is_measurable_on E by A113, Th48;
then A114: (f | E) + (g | E) is_measurable_on E by A112, A99, A111, MESFUNC2:7;
now
let r be real number ; :: thesis: DFPG /\ (less_dom (f + g),(R_EAL r)) in S
A115: E /\ (less_dom ((f | E) + (g | E)),(R_EAL r)) in S by A114, MESFUNC1:def 17;
DFPG \ (f " {+infty }) in S by A25, A31, PROB_1:12;
then A116: (g " {-infty }) /\ (DFPG \ (f " {+infty })) in S by A12, FINSUB_1:def 2;
DFPG \ (g " {+infty }) in S by A22, PROB_1:12;
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:9;
then A117: (E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ (((f " {-infty }) /\ (DFPG \ (g " {+infty }))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })))) in S by A115, PROB_1:9;
DFPG /\ (less_dom (f + g),(R_EAL r)) = ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty }))) by A47;
hence DFPG /\ (less_dom (f + g),(R_EAL r)) in S by A117, XBOOLE_1:4; :: thesis: verum
end;
then f + g is_measurable_on DFPG by MESFUNC1:def 17;
hence ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG ) ; :: thesis: verum