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 A1: ( 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 ) ; :: thesis: ex DFPG being Element of S st
( DFPG = dom (f + g) & f + g is_measurable_on DFPG )
consider E0 being Element of S such that
A2: ( E0 = dom f & f is_measurable_on E0 ) by A1;
A3: ( E0 /\ (eq_dom f,+infty ) in S & E0 /\ (eq_dom f,-infty ) in S ) by A2, MESFUNC1:37, MESFUNC1:38;

now

let v be set ; :: thesis: ( v in f " {+infty } implies v in E0 /\ (eq_dom f,+infty ) )
assume v in f " {+infty } ; :: thesis: v in E0 /\ (eq_dom f,+infty )
then ( v in dom f & f . v in {+infty } ) by FUNCT_1:def 13;
then ( v in dom f & f . v = +infty ) by TARSKI:def 1;
then ( v in E0 & v in eq_dom f,+infty ) by A2, MESFUNC1:def 16;
hence v in E0 /\ (eq_dom f,+infty ) by XBOOLE_0:def 4; :: thesis: verum

end;

then A4: f " {+infty } c= E0 /\ (eq_dom f,+infty ) by TARSKI:def 3;

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 A5: ( v in E0 & v in eq_dom f,+infty ) by XBOOLE_0:def 4;
then A6: v in dom f by MESFUNC1:def 16;
f . v = +infty by A5, MESFUNC1:def 16;
then f . v in {+infty } by TARSKI:def 1;
hence v in f " {+infty } by A6, FUNCT_1:def 13; :: thesis: verum

end;

then E0 /\ (eq_dom f,+infty ) c= f " {+infty } by TARSKI:def 3;
then A7: f " {+infty } = E0 /\ (eq_dom f,+infty ) by A4, XBOOLE_0:def 10;

now

let v be set ; :: thesis: ( v in f " {-infty } implies v in E0 /\ (eq_dom f,-infty ) )
assume v in f " {-infty } ; :: thesis: v in E0 /\ (eq_dom f,-infty )
then ( v in dom f & f . v in {-infty } ) by FUNCT_1:def 13;
then ( v in dom f & f . v = -infty ) by TARSKI:def 1;
then ( v in E0 & v in eq_dom f,-infty ) by A2, MESFUNC1:def 16;
hence v in E0 /\ (eq_dom f,-infty ) by XBOOLE_0:def 4; :: thesis: verum

end;

then A8: f " {-infty } c= E0 /\ (eq_dom f,-infty ) by TARSKI:def 3;

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 A9: ( v in E0 & v in eq_dom f,-infty ) by XBOOLE_0:def 4;
then A10: v in dom f by MESFUNC1:def 16;
f . v = -infty by A9, MESFUNC1:def 16;
then f . v in {-infty } by TARSKI:def 1;
hence v in f " {-infty } by A10, FUNCT_1:def 13; :: thesis: verum

end;

then A11: E0 /\ (eq_dom f,-infty ) c= f " {-infty } by TARSKI:def 3;
then A12: f " {-infty } = E0 /\ (eq_dom f,-infty ) by A8, XBOOLE_0:def 10;
A13: f " {-infty } in S by A3, A8, A11, XBOOLE_0:def 10;
consider Gf being Element of S such that
A14: ( Gf = dom g & g is_measurable_on Gf ) by A1;
A15: ( Gf /\ (eq_dom g,+infty ) in S & Gf /\ (eq_dom g,-infty ) in S ) by A14, MESFUNC1:37, MESFUNC1:38;

now

let v be set ; :: thesis: ( v in g " {+infty } implies v in Gf /\ (eq_dom g,+infty ) )
assume v in g " {+infty } ; :: thesis: v in Gf /\ (eq_dom g,+infty )
then ( v in dom g & g . v in {+infty } ) by FUNCT_1:def 13;
then ( v in dom g & g . v = +infty ) by TARSKI:def 1;
then ( v in Gf & v in eq_dom g,+infty ) by A14, MESFUNC1:def 16;
hence v in Gf /\ (eq_dom g,+infty ) by XBOOLE_0:def 4; :: thesis: verum

end;

then A16: 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 A17: ( v in Gf & v in eq_dom g,+infty ) by XBOOLE_0:def 4;
then A18: v in dom g by MESFUNC1:def 16;
g . v = +infty by A17, MESFUNC1:def 16;
then g . v in {+infty } by TARSKI:def 1;
hence v in g " {+infty } by A18, FUNCT_1:def 13; :: thesis: verum

end;

then Gf /\ (eq_dom g,+infty ) c= g " {+infty } by TARSKI:def 3;
then A19: g " {+infty } in S by A15, A16, XBOOLE_0:def 10;

now

let v be set ; :: thesis: ( v in g " {-infty } implies v in Gf /\ (eq_dom g,-infty ) )
assume v in g " {-infty } ; :: thesis: v in Gf /\ (eq_dom g,-infty )
then ( v in dom g & g . v in {-infty } ) by FUNCT_1:def 13;
then ( v in dom g & g . v = -infty ) by TARSKI:def 1;
then ( v in Gf & v in eq_dom g,-infty ) by A14, MESFUNC1:def 16;
hence v in Gf /\ (eq_dom g,-infty ) by XBOOLE_0:def 4; :: thesis: verum

end;

then A20: 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 A21: ( v in Gf & v in eq_dom g,-infty ) by XBOOLE_0:def 4;
then A22: v in dom g by MESFUNC1:def 16;
g . v = -infty by A21, MESFUNC1:def 16;
then g . v in {-infty } by TARSKI:def 1;
hence v in g " {-infty } by A22, FUNCT_1:def 13; :: thesis: verum

end;

then Gf /\ (eq_dom g,-infty ) c= g " {-infty } by TARSKI:def 3;
then A23: g " {-infty } in S by A15, A20, XBOOLE_0:def 10;
reconsider NF = (f " {+infty }) \/ (f " {-infty }) as Element of S by A3, A7, A13, PROB_1:41;
reconsider NG = (g " {+infty }) \/ (g " {-infty }) as Element of S by A19, A23, PROB_1:41;
reconsider NFG = NF \/ NG as Element of S ;
reconsider E = E0 \ NFG as Element of S ;
set f1 = f | E;
set g1 = g | E;
A24: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
( (f " {-infty }) /\ (g " {+infty }) c= f " {-infty } & f " {-infty } c= NF & (f " {+infty }) /\ (g " {-infty }) c= g " {-infty } & g " {-infty } c= NG ) by XBOOLE_1:7, XBOOLE_1:17;
then ( (f " {-infty }) /\ (g " {+infty }) c= NF & (f " {+infty }) /\ (g " {-infty }) c= NG ) by XBOOLE_1:1;
then ((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty })) c= NF \/ NG by XBOOLE_1:13;
then A25: E c= dom (f + g) by A1, A2, A24, XBOOLE_1:34;
then A26: ( (f + g) | E = (f | E) + (g | E) & dom ((f | E) + (g | E)) = E ) by Th35;
reconsider DFPG = dom (f + g) as Element of S by A1, A3, A7, A13, A19, A23, Th52;
A27: ( f is_measurable_on E & g is_measurable_on E ) by A1, A2, MESFUNC1:34, XBOOLE_1:36;
( (dom f) /\ E = E & (dom g) /\ E = E ) by A1, A2, XBOOLE_1:28, XBOOLE_1:36;
then A28: ( f | E is_measurable_on E & g | E is_measurable_on E ) by A27, Th48;

A29: now

let x be set ; :: thesis: ( x in dom (f | E) implies ( -infty < (f | E) . x & (f | E) . x < +infty ) )
assume A30: x in dom (f | E) ; :: thesis: ( -infty < (f | E) . x & (f | E) . x < +infty )
then x in (dom f) /\ E by RELAT_1:90;
then A31: ( x in dom f & x in E ) by XBOOLE_0:def 4;
then A32: not x in NFG by XBOOLE_0:def 5;
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;

A33: now

assume (f | E) . x = +infty ; :: thesis: contradiction
then f . x = +infty by A30, FUNCT_1:70;
then f . x in {+infty } by TARSKI:def 1;
then A34: x in ff " {+infty } by A31, FUNCT_2:46;
f " {+infty } c= NF by XBOOLE_1:7;
hence contradiction by A32, A34, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume (f | E) . x = -infty ; :: thesis: contradiction
then f . x = -infty by A30, FUNCT_1:70;
then ff . x in {-infty } by TARSKI:def 1;
then A35: x in ff " {-infty } by A31, FUNCT_2:46;
f " {-infty } c= NF by XBOOLE_1:7;
hence contradiction by A32, A35, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( -infty < (f | E) . x & (f | E) . x < +infty ) by A33, XXREAL_0:4, XXREAL_0:6; :: thesis: verum

end;

A36: now

let x be set ; :: thesis: ( x in dom (g | E) implies ( -infty < (g | E) . x & (g | E) . x < +infty ) )
assume A37: x in dom (g | E) ; :: thesis: ( -infty < (g | E) . x & (g | E) . x < +infty )
then x in (dom g) /\ E by RELAT_1:90;
then A38: ( x in dom g & x in E ) by XBOOLE_0:def 4;
then A39: not x in NFG by XBOOLE_0:def 5;
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;

A40: now

assume (g | E) . x = +infty ; :: thesis: contradiction
then g . x = +infty by A37, FUNCT_1:70;
then gg . x in {+infty } by TARSKI:def 1;
then A41: x in gg " {+infty } by A38, FUNCT_2:46;
g " {+infty } c= NG by XBOOLE_1:7;
hence contradiction by A39, A41, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume (g | E) . x = -infty ; :: thesis: contradiction
then g . x = -infty by A37, FUNCT_1:70;
then gg . x in {-infty } by TARSKI:def 1;
then A42: x in gg " {-infty } by A38, FUNCT_2:46;
g " {-infty } c= NG by XBOOLE_1:7;
hence contradiction by A39, A42, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( -infty < (g | E) . x & (g | E) . x < +infty ) by A40, 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 )
assume x in dom (f | E) ; :: thesis: |.((f | E) . x).| < +infty
then A43: ( -infty < (f | E) . x & (f | E) . x < +infty ) by A29;
- +infty = -infty by XXREAL_3:def 3;
hence |.((f | E) . x).| < +infty by A43, EXTREAL2:59; :: thesis: verum

end;

then A44: f | E is real-valued by MESFUNC2:def 1;

now

let x be Element of X; :: thesis: ( x in dom (g | E) implies |.((g | E) . x).| < +infty )
assume x in dom (g | E) ; :: thesis: |.((g | E) . x).| < +infty
then A45: ( -infty < (g | E) . x & (g | E) . x < +infty ) by A36;
- +infty = -infty by XXREAL_3:def 3;
hence |.((g | E) . x).| < +infty by A45, EXTREAL2:59; :: thesis: verum

end;

then g | E is real-valued by MESFUNC2:def 1;
then A46: ( E = dom ((f | E) + (g | E)) & (f | E) + (g | E) is_measurable_on E ) by A25, A28, A44, Th35, MESFUNC2:7;
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 DFPG /\ (less_dom (f + g),(R_EAL r)) implies b₁ in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty }))) )
assume x in DFPG /\ (less_dom (f + g),(R_EAL r)) ; :: thesis: b₁ in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })))
then A49: ( x in DFPG & x in less_dom (f + g),(R_EAL r) ) by XBOOLE_0:def 4;
then x in ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
then A50: ( not x in ((f " {+infty }) /\ (g " {-infty })) \/ ((f " {-infty }) /\ (g " {+infty })) & x in (dom f) /\ (dom g) ) by XBOOLE_0:def 5;
then A51: ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then A52: ( ( x in f " {+infty } implies f . x in {+infty } ) & ( f . x in {+infty } implies x in f " {+infty } ) & ( x in f " {-infty } implies f . x in {-infty } ) & ( f . x in {-infty } implies x in f " {-infty } ) & ( x in g " {+infty } implies g . x in {+infty } ) & ( g . x in {+infty } implies x in g " {+infty } ) & ( x in g " {-infty } implies g . x in {-infty } ) & ( g . x in {-infty } implies x in g " {-infty } ) ) by FUNCT_1:def 13;
then A53: ( ( x in f " {+infty } implies f . x = +infty ) & ( f . x = +infty implies x in f " {+infty } ) & ( x in f " {-infty } implies f . x = -infty ) & ( f . x = -infty implies x in f " {-infty } ) & ( x in g " {+infty } implies g . x = +infty ) & ( g . x = +infty implies x in g " {+infty } ) & ( x in g " {-infty } implies g . x = -infty ) & ( g . x = -infty implies x in g " {-infty } ) ) by TARSKI:def 1;
A54: (f + g) . x < R_EAL r by A49, MESFUNC1:def 12;
then A55: (f . x) + (g . x) < R_EAL r by A49, MESFUNC1:def 3;
A56: ( not x in (f " {+infty }) /\ (g " {-infty }) & not x in (f " {-infty }) /\ (g " {+infty }) ) by A50, XBOOLE_0:def 3;

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

suppose f . x = -infty ; :: thesis: b₁ in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })))

then ( x in f " {-infty } & x in DFPG \ (g " {+infty }) ) by A49, A52, A56, TARSKI:def 1, XBOOLE_0:def 4, XBOOLE_0:def 5;
then x in (f " {-infty }) /\ (DFPG \ (g " {+infty })) by 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 A57: f . x <> -infty ; :: thesis: b₁ 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 g . x = -infty ; :: thesis: b₁ in ((E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ ((f " {-infty }) /\ (DFPG \ (g " {+infty })))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })))

then ( x in g " {-infty } & x in DFPG \ (f " {+infty }) ) by A49, A52, A56, TARSKI:def 1, XBOOLE_0:def 4, XBOOLE_0:def 5;
then x in (g " {-infty }) /\ (DFPG \ (f " {+infty })) by 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 g . x <> -infty ; :: thesis: b₁ 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 }) & not x in g " {-infty } & not x in g " {+infty } ) by A53, A55, A57, XBOOLE_0:def 3, XXREAL_3:63;
then ( not x in ((f " {-infty }) \/ (f " {+infty })) \/ (g " {-infty }) & not x in g " {+infty } ) by XBOOLE_0:def 3;
then not x in (((f " {-infty }) \/ (f " {+infty })) \/ (g " {-infty })) \/ (g " {+infty }) by XBOOLE_0:def 3;
then not x in NFG by XBOOLE_1:4;
then A58: x in E by A2, A51, XBOOLE_0:def 5;
then ((f | E) + (g | E)) . x = (f + g) . x by A26, FUNCT_1:70;
then x in less_dom ((f | E) + (g | E)),(R_EAL r) by A46, A54, A58, MESFUNC1:def 12;
then x in E /\ (less_dom ((f | E) + (g | E)),(R_EAL r)) by A58, 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;

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 b₁ 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: b₁ in DFPG /\ (less_dom (f + g),(R_EAL r))
then A59: ( 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 A59, XBOOLE_0:def 3;

suppose x in E /\ (less_dom ((f | E) + (g | E)),(R_EAL r)) ; :: thesis: b₁ in DFPG /\ (less_dom (f + g),(R_EAL r))

then A60: ( x in E & x in less_dom ((f | E) + (g | E)),(R_EAL r) ) by 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 A26, A60, FUNCT_1:70;
then x in less_dom (f + g),(R_EAL r) by A25, A60, MESFUNC1:def 12;
hence x in DFPG /\ (less_dom (f + g),(R_EAL r)) by A25, A60, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A61: ( x in (f " {-infty }) /\ (DFPG \ (g " {+infty })) or x in (g " {-infty }) /\ (DFPG \ (f " {+infty })) ) ; :: thesis: b₁ 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 A61;

suppose x in (f " {-infty }) /\ (DFPG \ (g " {+infty })) ; :: thesis: b₁ in DFPG /\ (less_dom (f + g),(R_EAL r))

then A62: ( x in f " {-infty } & x in DFPG \ (g " {+infty }) ) by XBOOLE_0:def 4;
then A63: 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 x in (dom f) /\ (dom g) by XBOOLE_0:def 5;
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then ( ( x in f " {+infty } implies f . x in {+infty } ) & ( f . x in {+infty } implies x in f " {+infty } ) & ( x in f " {-infty } implies f . x in {-infty } ) & ( f . x in {-infty } implies x in f " {-infty } ) & ( x in g " {+infty } implies g . x in {+infty } ) & ( g . x in {+infty } implies x in g " {+infty } ) & ( x in g " {-infty } implies g . x in {-infty } ) & ( g . x in {-infty } implies x in g " {-infty } ) ) by FUNCT_1:def 13;
then ( ( x in f " {+infty } implies f . x = +infty ) & ( f . x = +infty implies x in f " {+infty } ) & ( x in f " {-infty } implies f . x = -infty ) & ( f . x = -infty implies x in f " {-infty } ) & ( x in g " {+infty } implies g . x = +infty ) & ( g . x = +infty implies x in g " {+infty } ) & ( x in g " {-infty } implies g . x = -infty ) & ( g . x = -infty implies x in g " {-infty } ) ) by TARSKI:def 1;
then A64: (f . x) + (g . x) = -infty by A62, XBOOLE_0:def 5, XXREAL_3:def 2;
R_EAL r in REAL by XREAL_0:def 1;
then -infty < R_EAL r by XXREAL_0:12;
then (f + g) . x < R_EAL r by A63, A64, MESFUNC1:def 3;
then x in less_dom (f + g),(R_EAL r) by A63, MESFUNC1:def 12;
hence x in DFPG /\ (less_dom (f + g),(R_EAL r)) by A63, XBOOLE_0:def 4; :: thesis: verum

end;

suppose x in (g " {-infty }) /\ (DFPG \ (f " {+infty })) ; :: thesis: b₁ in DFPG /\ (less_dom (f + g),(R_EAL r))

then A65: ( x in g " {-infty } & x in DFPG \ (f " {+infty }) ) by XBOOLE_0:def 4;
then A66: 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 x in (dom f) /\ (dom g) by XBOOLE_0:def 5;
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then ( ( x in f " {+infty } implies f . x in {+infty } ) & ( f . x in {+infty } implies x in f " {+infty } ) & ( x in f " {-infty } implies f . x in {-infty } ) & ( f . x in {-infty } implies x in f " {-infty } ) & ( x in g " {+infty } implies g . x in {+infty } ) & ( g . x in {+infty } implies x in g " {+infty } ) & ( x in g " {-infty } implies g . x in {-infty } ) & ( g . x in {-infty } implies x in g " {-infty } ) ) by FUNCT_1:def 13;
then ( ( x in f " {+infty } implies f . x = +infty ) & ( f . x = +infty implies x in f " {+infty } ) & ( x in f " {-infty } implies f . x = -infty ) & ( f . x = -infty implies x in f " {-infty } ) & ( x in g " {+infty } implies g . x = +infty ) & ( g . x = +infty implies x in g " {+infty } ) & ( x in g " {-infty } implies g . x = -infty ) & ( g . x = -infty implies x in g " {-infty } ) ) by TARSKI:def 1;
then A67: ( (f . x) + (g . x) = -infty & x in DFPG ) by A65, XBOOLE_0:def 5, XXREAL_3:def 2;
R_EAL r in REAL by XREAL_0:def 1;
then -infty < R_EAL r by XXREAL_0:12;
then ( (f + g) . x < R_EAL r & x in DFPG ) by A67, MESFUNC1:def 3;
then x in less_dom (f + g),(R_EAL r) by MESFUNC1:def 12;
hence x in DFPG /\ (less_dom (f + g),(R_EAL r)) by A66, XBOOLE_0:def 4; :: 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;

now

let r be real number ; :: thesis: DFPG /\ (less_dom (f + g),(R_EAL r)) in S
A68: 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;
( DFPG \ (g " {+infty }) in S & DFPG \ (f " {+infty }) in S ) by A3, A7, A19, PROB_1:44;
then ( (f " {-infty }) /\ (DFPG \ (g " {+infty })) in S & (g " {-infty }) /\ (DFPG \ (f " {+infty })) in S ) by A3, A12, A23, FINSUB_1:def 2;
then A69: ((f " {-infty }) /\ (DFPG \ (g " {+infty }))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty }))) in S by PROB_1:41;
E /\ (less_dom ((f | E) + (g | E)),(R_EAL r)) in S by A46, MESFUNC1:def 17;
then (E /\ (less_dom ((f | E) + (g | E)),(R_EAL r))) \/ (((f " {-infty }) /\ (DFPG \ (g " {+infty }))) \/ ((g " {-infty }) /\ (DFPG \ (f " {+infty })))) in S by A69, PROB_1:41;
hence DFPG /\ (less_dom (f + g),(R_EAL r)) in S by A68, 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