let f, g be PartFunc of REAL,REAL; :: thesis: ( dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = +infty ) & ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = -infty ) implies ( f - g is_improper_integrable_on_REAL & improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) - (improper_integral_on_REAL g) ) )
assume that
A1: dom f = REAL and
A2: dom g = REAL and
A3: f is_improper_integrable_on_REAL and
A4: g is_improper_integrable_on_REAL and
A5: ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = +infty ) and
A6: ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = -infty ) ; :: thesis: ( f - g is_improper_integrable_on_REAL & improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) - (improper_integral_on_REAL g) )
A7: dom (- g) = dom g by VALUED_1:8;
A8: - g is_improper_integrable_on_REAL by A2, A4, Th50;
A9: improper_integral_on_REAL (- g) = - (improper_integral_on_REAL g) by A2, A4, Th50;
A10: ( improper_integral_on_REAL f <> +infty or improper_integral_on_REAL (- g) <> -infty ) by A5, A9, XXREAL_3:23;
A11: ( improper_integral_on_REAL f <> -infty or improper_integral_on_REAL (- g) <> +infty ) by A6, A9, XXREAL_3:23;
hence f - g is_improper_integrable_on_REAL by A1, A2, A3, A7, A8, A10, Th51; :: thesis: improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) - (improper_integral_on_REAL g)
improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL (- g)) by A1, A2, A3, A7, A8, A10, A11, Th51;
then improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) + (- (improper_integral_on_REAL g)) by A2, A4, Th50;
hence improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) - (improper_integral_on_REAL g) by XXREAL_3:def 4; :: thesis: verum