let f, g be PartFunc of REAL,REAL; :: thesis: for a, b being Real st ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = -infty ) & ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = +infty ) holds
( f + g is_improper_integrable_on a,b & improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) )
let a, b be Real; :: thesis: ( ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = -infty ) & ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = +infty ) implies ( f + g is_improper_integrable_on a,b & improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) ) )
assume that
A1: ].a,b.[ c= dom f and
A2: ].a,b.[ c= dom g and
A3: f is_improper_integrable_on a,b and
A4: g is_improper_integrable_on a,b and
A5: ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = -infty ) and
A6: ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = +infty ) ; :: thesis: ( f + g is_improper_integrable_on a,b & improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) )
consider c being Real such that
A7: ( a < c & c < b ) and
A8: f is_left_improper_integrable_on a,c and
A9: f is_right_improper_integrable_on c,b and
A10: ( not left_improper_integral (f,a,c) = -infty or not right_improper_integral (f,c,b) = +infty ) and
A11: ( not left_improper_integral (f,a,c) = +infty or not right_improper_integral (f,c,b) = -infty ) by A3;
consider c1 being Real such that
A12: ( a < c1 & c1 < b ) and
A13: g is_left_improper_integrable_on a,c1 and
A14: g is_right_improper_integrable_on c1,b and
A15: ( not left_improper_integral (g,a,c1) = -infty or not right_improper_integral (g,c1,b) = +infty ) and
A16: ( not left_improper_integral (g,a,c1) = +infty or not right_improper_integral (g,c1,b) = -infty ) by A4;
( ].a,c.] c= ].a,b.[ & [.c,b.[ c= ].a,b.[ & ].a,c1.] c= ].a,b.[ & [.c1,b.[ c= ].a,b.[ ) by A7, A12, XXREAL_1:48, XXREAL_1:49;
then A17: ( ].a,c.] c= dom f & ].a,c.] c= dom g & [.c,b.[ c= dom f & [.c,b.[ c= dom g & ].a,c1.] c= dom f & ].a,c1.] c= dom g & [.c1,b.[ c= dom f & [.c1,b.[ c= dom g ) by A1, A2;
A18: g is_left_improper_integrable_on a,c

proof

per cases ( c < c1 or c1 <= c ) ;

suppose c < c1 ; :: thesis: g is_left_improper_integrable_on a,c

hence g is_left_improper_integrable_on a,c by A7, A17, A13, Th37; :: thesis: verum

end;

suppose A19: c1 <= c ; :: thesis: g is_left_improper_integrable_on a,c

( g | ['c1,c'] is bounded & g is_integrable_on ['c1,c'] ) by A19, A7, A14;
hence g is_left_improper_integrable_on a,c by A12, A19, A17, A13, Th38; :: thesis: verum

end;

end;

end;

A20: g is_right_improper_integrable_on c,b

proof

per cases ( c < c1 or c1 <= c ) ;

suppose A21: c < c1 ; :: thesis: g is_right_improper_integrable_on c,b

( g | ['c,c1'] is bounded & g is_integrable_on ['c,c1'] ) by A21, A7, A13;
hence g is_right_improper_integrable_on c,b by A21, A12, A17, A14, Th43; :: thesis: verum

end;

suppose c1 <= c ; :: thesis: g is_right_improper_integrable_on c,b

hence g is_right_improper_integrable_on c,b by A7, A17, A14, Th42; :: thesis: verum

end;

end;

end;

A22: ( not left_improper_integral (g,a,c) = -infty or not right_improper_integral (g,c,b) = +infty )

proof

per cases ( c < c1 or c1 <= c ) ;

suppose A23: c < c1 ; :: thesis: ( not left_improper_integral (g,a,c) = -infty or not right_improper_integral (g,c,b) = +infty )

then A24: ( g | ['c,c1'] is bounded & g is_integrable_on ['c,c1'] ) by A7, A13;
A25: g is_left_improper_integrable_on a,c by A7, A23, A17, A13, Th37;
g is_right_improper_integrable_on c,b by A23, A12, A17, A24, A14, Th43;
hence ( not left_improper_integral (g,a,c) = -infty or not right_improper_integral (g,c,b) = +infty ) by A15, A12, A17, A7, A23, A24, A25, Th38, Th42; :: thesis: verum

end;

suppose A26: c1 <= c ; :: thesis: ( not left_improper_integral (g,a,c) = -infty or not right_improper_integral (g,c,b) = +infty )

A27: ( g | ['c1,c'] is bounded & g is_integrable_on ['c1,c'] ) by A26, A7, A14;
then A28: g is_left_improper_integrable_on a,c by A12, A26, A17, A13, Th38;
g is_right_improper_integrable_on c,b by A26, A7, A17, A14, Th42;
hence ( not left_improper_integral (g,a,c) = -infty or not right_improper_integral (g,c,b) = +infty ) by A15, A7, A17, A27, A12, A26, A28, Th37, Th43; :: thesis: verum

end;

end;

end;

A29: ( not left_improper_integral (g,a,c) = +infty or not right_improper_integral (g,c,b) = -infty )

proof

per cases ( c < c1 or c1 <= c ) ;

suppose A30: c < c1 ; :: thesis: ( not left_improper_integral (g,a,c) = +infty or not right_improper_integral (g,c,b) = -infty )

then A31: ( g | ['c,c1'] is bounded & g is_integrable_on ['c,c1'] ) by A7, A13;
A32: g is_left_improper_integrable_on a,c by A7, A30, A17, A13, Th37;
g is_right_improper_integrable_on c,b by A30, A12, A17, A31, A14, Th43;
hence ( not left_improper_integral (g,a,c) = +infty or not right_improper_integral (g,c,b) = -infty ) by A16, A12, A17, A7, A30, A31, A32, Th38, Th42; :: thesis: verum

end;

suppose A33: c1 <= c ; :: thesis: ( not left_improper_integral (g,a,c) = +infty or not right_improper_integral (g,c,b) = -infty )

then A34: ( g | ['c1,c'] is bounded & g is_integrable_on ['c1,c'] ) by A7, A14;
then A35: g is_left_improper_integrable_on a,c by A12, A33, A17, A13, Th38;
g is_right_improper_integrable_on c,b by A33, A7, A17, A14, Th42;
hence ( not left_improper_integral (g,a,c) = +infty or not right_improper_integral (g,c,b) = -infty ) by A16, A7, A17, A34, A12, A33, A35, Th37, Th43; :: thesis: verum

end;

end;

end;

A36: improper_integral (f,a,b) = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) by A1, A3, A7, Th48;
A37: improper_integral (g,a,b) = (left_improper_integral (g,a,c)) + (right_improper_integral (g,c,b)) by A2, A4, A7, Th48;
then A38: ( not left_improper_integral (f,a,c) = +infty or not left_improper_integral (g,a,c) = -infty ) by A5, A36, A11, A22, XXREAL_3:def 2;
A39: ( not left_improper_integral (f,a,c) = -infty or not left_improper_integral (g,a,c) = +infty ) by A6, A36, A37, A10, A29, XXREAL_3:def 2;
A40: ( not right_improper_integral (f,c,b) = +infty or not right_improper_integral (g,c,b) = -infty ) by A5, A36, A37, A10, A29, XXREAL_3:def 2;
A41: ( not right_improper_integral (f,c,b) = -infty or not right_improper_integral (g,c,b) = +infty ) by A6, A36, A37, A11, A22, XXREAL_3:def 2;
A42: f + g is_left_improper_integrable_on a,c by A7, A8, A18, A17, A38, A39, Th57;
A43: left_improper_integral ((f + g),a,c) = (left_improper_integral (f,a,c)) + (left_improper_integral (g,a,c)) by A7, A17, A8, A18, A38, A39, Th57;
A44: f + g is_right_improper_integrable_on c,b by A7, A17, A9, A20, A40, A41, Th58;
A45: right_improper_integral ((f + g),c,b) = (right_improper_integral (f,c,b)) + (right_improper_integral (g,c,b)) by A7, A17, A9, A20, A40, A41, Th58;

A46: now :: thesis: ( left_improper_integral ((f + g),a,c) = -infty implies not right_improper_integral ((f + g),c,b) = +infty )

assume A47: ( left_improper_integral ((f + g),a,c) = -infty & right_improper_integral ((f + g),c,b) = +infty ) ; :: thesis: contradiction

per cases ( ( left_improper_integral (f,a,c) = -infty & right_improper_integral (g,c,b) = +infty ) or ( left_improper_integral (g,a,c) = -infty & right_improper_integral (f,c,b) = +infty ) ) by A10, A22, A43, A45, A47, XXREAL_3:16, XXREAL_3:17;

suppose ( left_improper_integral (f,a,c) = -infty & right_improper_integral (g,c,b) = +infty ) ; :: thesis: contradiction

hence contradiction by A6, A10, A36, A37, A22, XXREAL_3:def 2; :: thesis: verum

end;

suppose ( left_improper_integral (g,a,c) = -infty & right_improper_integral (f,c,b) = +infty ) ; :: thesis: contradiction

hence contradiction by A5, A10, A36, A37, A22, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

A48: now :: thesis: ( left_improper_integral ((f + g),a,c) = +infty implies not right_improper_integral ((f + g),c,b) = -infty )

assume A49: ( left_improper_integral ((f + g),a,c) = +infty & right_improper_integral ((f + g),c,b) = -infty ) ; :: thesis: contradiction

per cases ( ( left_improper_integral (f,a,c) = +infty & right_improper_integral (g,c,b) = -infty ) or ( left_improper_integral (g,a,c) = +infty & right_improper_integral (f,c,b) = -infty ) ) by A11, A29, A45, A49, A43, XXREAL_3:16, XXREAL_3:17;

suppose ( left_improper_integral (f,a,c) = +infty & right_improper_integral (g,c,b) = -infty ) ; :: thesis: contradiction

hence contradiction by A5, A11, A36, A37, A29, XXREAL_3:def 2; :: thesis: verum

end;

suppose ( left_improper_integral (g,a,c) = +infty & right_improper_integral (f,c,b) = -infty ) ; :: thesis: contradiction

hence contradiction by A6, A11, A36, A37, A29, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

hence A50: f + g is_improper_integrable_on a,b by A7, A42, A44, A46; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then ].a,b.[ c= dom (f + g) by A1, A2, XBOOLE_1:19;
then A51: improper_integral ((f + g),a,b) = (left_improper_integral ((f + g),a,c)) + (right_improper_integral ((f + g),c,b)) by A7, A50, Th48;

per cases ( left_improper_integral ((f + g),a,c) = +infty or left_improper_integral ((f + g),a,c) = -infty or left_improper_integral ((f + g),a,c) in REAL ) by XXREAL_0:14;

suppose A52: left_improper_integral ((f + g),a,c) = +infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then A53: ( left_improper_integral (f,a,c) = +infty or left_improper_integral (g,a,c) = +infty ) by A43, XXREAL_3:16;
A54: improper_integral ((f + g),a,b) = +infty by A52, A48, A51, XXREAL_3:def 2;

per cases ( left_improper_integral (f,a,c) = +infty or left_improper_integral (g,a,c) = +infty ) by A53;

suppose left_improper_integral (f,a,c) = +infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then improper_integral (f,a,b) = +infty by A11, A36, XXREAL_3:def 2;
hence improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) by A5, A54, XXREAL_3:def 2; :: thesis: verum

end;

suppose left_improper_integral (g,a,c) = +infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then improper_integral (g,a,b) = +infty by A37, A29, XXREAL_3:def 2;
hence improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) by A6, A54, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A55: left_improper_integral ((f + g),a,c) = -infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then A56: ( left_improper_integral (f,a,c) = -infty or left_improper_integral (g,a,c) = -infty ) by A43, XXREAL_3:17;
right_improper_integral ((f + g),c,b) <> +infty by A55, A46;
then A57: improper_integral ((f + g),a,b) = -infty by A55, A51, XXREAL_3:def 2;

per cases ( left_improper_integral (f,a,c) = -infty or left_improper_integral (g,a,c) = -infty ) by A56;

suppose left_improper_integral (f,a,c) = -infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then improper_integral (f,a,b) = -infty by A10, A36, XXREAL_3:def 2;
hence improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) by A6, A57, XXREAL_3:def 2; :: thesis: verum

end;

suppose left_improper_integral (g,a,c) = -infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then improper_integral (g,a,b) = -infty by A22, A37, XXREAL_3:def 2;
hence improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) by A5, A57, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A58: left_improper_integral ((f + g),a,c) in REAL ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then A59: ( left_improper_integral (f,a,c) in REAL & left_improper_integral (g,a,c) in REAL ) by A38, A39, A43, XXREAL_3:20;
then reconsider lf = left_improper_integral (f,a,c), lg = left_improper_integral (g,a,c) as Real ;

per cases ( right_improper_integral ((f + g),c,b) = +infty or right_improper_integral ((f + g),c,b) = -infty or right_improper_integral ((f + g),c,b) in REAL ) by XXREAL_0:14;

suppose A60: right_improper_integral ((f + g),c,b) = +infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then ( right_improper_integral (f,c,b) = +infty or right_improper_integral (g,c,b) = +infty ) by A45, XXREAL_3:16;
then ( improper_integral (f,a,b) = +infty or improper_integral (g,a,b) = +infty ) by A59, A36, A37, XXREAL_3:def 2;
then (improper_integral (f,a,b)) + (improper_integral (g,a,b)) = +infty by A5, A6, XXREAL_3:def 2;
hence improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) by A58, A60, A51, XXREAL_3:def 2; :: thesis: verum

end;

suppose A61: right_improper_integral ((f + g),c,b) = -infty ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then ( right_improper_integral (f,c,b) = -infty or right_improper_integral (g,c,b) = -infty ) by A45, XXREAL_3:17;
then ( improper_integral (f,a,b) = -infty or improper_integral (g,a,b) = -infty ) by A59, A36, A37, XXREAL_3:def 2;
then (improper_integral (f,a,b)) + (improper_integral (g,a,b)) = -infty by A5, A6, XXREAL_3:def 2;
hence improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) by A58, A61, A51, XXREAL_3:def 2; :: thesis: verum

end;

suppose right_improper_integral ((f + g),c,b) in REAL ; :: thesis: improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b))

then ( right_improper_integral (f,c,b) in REAL & right_improper_integral (g,c,b) in REAL ) by A40, A41, A45, XXREAL_3:20;
then reconsider rf = right_improper_integral (f,c,b), rg = right_improper_integral (g,c,b) as Real ;
( improper_integral (f,a,b) = lf + rf & improper_integral (g,a,b) = lg + rg ) by A36, A37, XXREAL_3:def 2;
then A62: (improper_integral (f,a,b)) + (improper_integral (g,a,b)) = (lf + rf) + (lg + rg) by XXREAL_3:def 2;
( left_improper_integral ((f + g),a,c) = lf + lg & right_improper_integral ((f + g),c,b) = rf + rg ) by A43, A45, XXREAL_3:def 2;
then improper_integral ((f + g),a,b) = (lf + lg) + (rf + rg) by A51, XXREAL_3:def 2;
hence improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) by A62; :: thesis: verum

end;

end;

end;

end;