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;

Gf /\ (eq_dom (g,-infty)) in S by A5, MESFUNC1:34;

then A12: g " {-infty} in S by A8, A11, XBOOLE_0:def 10;

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;

then A31: f " {+infty} = E0 /\ (eq_dom (f,+infty)) by A28;

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})))

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;

hence ex DFPG being Element of S st

( DFPG = dom (f + g) & f + g is DFPG -measurable ) ; :: thesis: verum

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))

then A8:
g " {-infty} c= Gf /\ (eq_dom (g,-infty))
;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;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

now :: thesis: for v being object st v in Gf /\ (eq_dom (g,-infty)) holds

v in g " {-infty}

then A11:
Gf /\ (eq_dom (g,-infty)) c= g " {-infty}
;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;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

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))

then A15:
g " {+infty} c= Gf /\ (eq_dom (g,+infty))
;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;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

now :: thesis: for v being object st v in Gf /\ (eq_dom (g,+infty)) holds

v in g " {+infty}

then A18:
Gf /\ (eq_dom (g,+infty)) c= g " {+infty}
;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;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

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}

then A28:
E0 /\ (eq_dom (f,+infty)) c= f " {+infty}
;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;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

now :: thesis: for v being object st v in f " {+infty} holds

v in E0 /\ (eq_dom (f,+infty))

then
f " {+infty} c= E0 /\ (eq_dom (f,+infty))
;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;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

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}

then A34:
E0 /\ (eq_dom (f,-infty)) c= f " {-infty}
;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;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

now :: thesis: for v being object st v in f " {-infty} holds

v in E0 /\ (eq_dom (f,-infty))

then A37:
f " {-infty} c= E0 /\ (eq_dom (f,-infty))
;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;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

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})));

end;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))

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 b_{1} 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: b_{1} 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;

end;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: b

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;

end;

suppose A50:
x in E /\ (less_dom (((f | E) + (g | E)),r))
; :: thesis: b_{1} 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;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

suppose A52:
( x in (f " {-infty}) /\ (DFPG \ (g " {+infty})) or x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) )
; :: thesis: b_{1} in DFPG /\ (less_dom ((f + g),r))

end;

per cases
( x in (f " {-infty}) /\ (DFPG \ (g " {+infty})) or x in (g " {-infty}) /\ (DFPG \ (f " {+infty})) )
by A52;

end;

suppose A53:
x in (f " {-infty}) /\ (DFPG \ (g " {+infty}))
; :: thesis: b_{1} 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;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

suppose A59:
x in (g " {-infty}) /\ (DFPG \ (f " {+infty}))
; :: thesis: b_{1} 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;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

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})))

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: verumx 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 b_{1} 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: b_{1} 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;

end;reconsider xx = x as set by TARSKI:1;

assume A66: x in DFPG /\ (less_dom ((f + g),r)) ; :: thesis: b

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 )
;

end;

suppose A83:
f . x = -infty
; :: thesis: b_{1} 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;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

suppose A84:
f . x <> -infty
; :: thesis: b_{1} in ((E /\ (less_dom (((f | E) + (g | E)),r))) \/ ((f " {-infty}) /\ (DFPG \ (g " {+infty})))) \/ ((g " {-infty}) /\ (DFPG \ (f " {+infty})))

end;

per cases
( g . x = -infty or g . x <> -infty )
;

end;

suppose A85:
g . x = -infty
; :: thesis: b_{1} 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;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

suppose A86:
g . x <> -infty
; :: thesis: b_{1} 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;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

A88: now :: thesis: for x being set st x in dom (f | E) holds

( -infty < (f | E) . x & (f | E) . x < +infty )

( -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;

end;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;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

now :: thesis: not (f | E) . x = +infty

hence
( -infty < (f | E) . x & (f | E) . x < +infty )
by A93, XXREAL_0:4, XXREAL_0:6; :: thesis: verumassume
(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;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

now :: thesis: for x being Element of X st x in dom (f | E) holds

|.((f | E) . x).| < +infty

then A99:
f | E is real-valued
by MESFUNC2:def 1;|.((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;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

A100: now :: thesis: for x being set st x in dom (g | E) holds

( -infty < (g | E) . x & (g | E) . x < +infty )

( -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;

end;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;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

now :: thesis: not (g | E) . x = +infty

hence
( -infty < (g | E) . x & (g | E) . x < +infty )
by A105, XXREAL_0:4, XXREAL_0:6; :: thesis: verumassume
(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;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

now :: thesis: for x being Element of X st x in dom (g | E) holds

|.((g | E) . x).| < +infty

then A111:
g | E is real-valued
by MESFUNC2:def 1;|.((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;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

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

then
f + g is DFPG -measurable
by MESFUNC1:def 16;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;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

hence ex DFPG being Element of S st

( DFPG = dom (f + g) & f + g is DFPG -measurable ) ; :: thesis: verum