integr10.miz



    begin

    reserve a,b,r,g for Real;

    theorem :: INTEGR10:1

    

     Th1: for a,b,g1,M be Real st a < b & 0 < g1 & 0 < M holds ex r st a < r & r < b & ((b - r) * M) < g1

    proof

      let a,b,g1,M be Real such that

       A1: a < b and

       A2: 0 < g1 and

       A3: 0 < M;

      set r3 = ( max (a,(b - (g1 / M))));

      (b - (g1 / M)) < b by A2, A3, XREAL_1: 44, XREAL_1: 139;

      then r3 < b by A1, XXREAL_0: 16;

      then

      consider q be Real such that

       A4: r3 < q and

       A5: q < b by XREAL_1: 5;

      reconsider r = q as Real;

      take r;

      (b - (g1 / M)) <= r3 by XXREAL_0: 25;

      then (b - (g1 / M)) < r by A4, XXREAL_0: 2;

      then ((b - (g1 / M)) - (r - (g1 / M))) < (r - (r - (g1 / M))) by XREAL_1: 14;

      then ((b - r) * 1) < (g1 / M);

      then a <= r3 & ((b - r) * M) < (g1 / 1) by A3, XREAL_1: 111, XXREAL_0: 25;

      hence thesis by A4, A5, XXREAL_0: 2;

    end;

    theorem :: INTEGR10:2

    

     Th2: for a,b,g1,M be Real st a < b & 0 < g1 & 0 < M holds ex r st a < r & r < b & ((r - a) * M) < g1

    proof

      let a,b,g1,M be Real such that

       A1: a < b and

       A2: 0 < g1 & 0 < M;

      ( - b) < ( - a) by A1, XREAL_1: 24;

      then

      consider r1 be Real such that

       A3: ( - b) < r1 & r1 < ( - a) and

       A4: ((( - a) - r1) * M) < g1 by A2, Th1;

      reconsider r = ( - r1) as Real;

      take r;

      ( - ( - b)) > ( - r1) & ( - r1) > ( - ( - a)) by A3, XREAL_1: 24;

      hence thesis by A4;

    end;

    theorem :: INTEGR10:3

    (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

    proof

      

       A1: ( min (a,b)) <= a by XXREAL_0: 17;

      

       A2: [.( min (a,b)), ( max (a,b)).] c= REAL ;

      ( exp_R | REAL ) is continuous & a <= ( max (a,b)) by XXREAL_0: 25;

      then

       A3: ( exp_R . ( max (a,b))) = (( integral ( exp_R ,( min (a,b)),( max (a,b)))) + ( exp_R . ( min (a,b)))) by A1, A2, INTEGRA7: 20, INTEGRA7: 27, SIN_COS: 47, XXREAL_0: 2;

      

       A4: ( min (a,b)) = a implies (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

      proof

        assume

         A5: ( min (a,b)) = a;

        then ( max (a,b)) = b by XXREAL_0: 36;

        hence thesis by A3, A5;

      end;

      ( min (a,b)) = b implies (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

      proof

        assume

         A6: ( min (a,b)) = b;

        then

         A7: ( max (a,b)) = a by XXREAL_0: 36;

        b < a implies (( exp_R . b) - ( exp_R . a)) = ( integral ( exp_R ,a,b))

        proof

          assume b < a;

          then ( integral ( exp_R ,a,b)) = ( - ( integral ( exp_R , ['b, a']))) by INTEGRA5:def 4;

          then ( exp_R . a) = (( - ( integral ( exp_R ,a,b))) + ( exp_R . b)) by A1, A3, A6, A7, INTEGRA5:def 4;

          hence thesis;

        end;

        hence thesis by A1, A4, A6, XXREAL_0: 1;

      end;

      hence thesis by A4, XXREAL_0: 15;

    end;

    begin

    definition

      let f be PartFunc of REAL , REAL ;

      let a,b be Real;

      :: INTEGR10:def1

      pred f is_right_ext_Riemann_integrable_on a,b means (for d be Real st a <= d & d < b holds f is_integrable_on ['a, d'] & (f | ['a, d']) is bounded) & ex Intf be PartFunc of REAL , REAL st ( dom Intf) = [.a, b.[ & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x))) & Intf is_left_convergent_in b;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let a,b be Real;

      :: INTEGR10:def2

      pred f is_left_ext_Riemann_integrable_on a,b means (for d be Real st a < d & d <= b holds f is_integrable_on ['d, b'] & (f | ['d, b']) is bounded) & ex Intf be PartFunc of REAL , REAL st ( dom Intf) = ].a, b.] & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b))) & Intf is_right_convergent_in a;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let a,b be Real;

      assume

       A1: f is_right_ext_Riemann_integrable_on (a,b);

      :: INTEGR10:def3

      func ext_right_integral (f,a,b) -> Real means

      : Def3: ex Intf be PartFunc of REAL , REAL st ( dom Intf) = [.a, b.[ & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x))) & Intf is_left_convergent_in b & it = ( lim_left (Intf,b));

      existence

      proof

        consider Intf be PartFunc of REAL , REAL such that

         A2: (( dom Intf) = [.a, b.[ & for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x))) & Intf is_left_convergent_in b by A1;

        take ( lim_left (Intf,b));

        thus thesis by A2;

      end;

      uniqueness

      proof

        let y1,y2 be Real;

        assume ex Intf1 be PartFunc of REAL , REAL st ( dom Intf1) = [.a, b.[ & (for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,a,x))) & Intf1 is_left_convergent_in b & y1 = ( lim_left (Intf1,b));

        then

        consider Intf1 be PartFunc of REAL , REAL such that

         A3: ( dom Intf1) = [.a, b.[ and

         A4: for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,a,x)) and Intf1 is_left_convergent_in b and

         A5: y1 = ( lim_left (Intf1,b));

        assume ex Intf2 be PartFunc of REAL , REAL st ( dom Intf2) = [.a, b.[ & (for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,a,x))) & Intf2 is_left_convergent_in b & y2 = ( lim_left (Intf2,b));

        then

        consider Intf2 be PartFunc of REAL , REAL such that

         A6: ( dom Intf2) = [.a, b.[ and

         A7: for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,a,x)) and Intf2 is_left_convergent_in b and

         A8: y2 = ( lim_left (Intf2,b));

        now

          let x be Element of REAL ;

          assume

           A9: x in ( dom Intf1);

          

          hence (Intf1 . x) = ( integral (f,a,x)) by A4

          .= (Intf2 . x) by A3, A6, A7, A9;

        end;

        hence thesis by A3, A5, A6, A8, PARTFUN1: 5;

      end;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let a,b be Real;

      assume

       A1: f is_left_ext_Riemann_integrable_on (a,b);

      :: INTEGR10:def4

      func ext_left_integral (f,a,b) -> Real means

      : Def4: ex Intf be PartFunc of REAL , REAL st ( dom Intf) = ].a, b.] & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b))) & Intf is_right_convergent_in a & it = ( lim_right (Intf,a));

      existence

      proof

        consider Intf be PartFunc of REAL , REAL such that

         A2: (( dom Intf) = ].a, b.] & for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b))) & Intf is_right_convergent_in a by A1;

        take ( lim_right (Intf,a));

        thus thesis by A2;

      end;

      uniqueness

      proof

        let y1,y2 be Real;

        assume ex Intf1 be PartFunc of REAL , REAL st ( dom Intf1) = ].a, b.] & (for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,x,b))) & Intf1 is_right_convergent_in a & y1 = ( lim_right (Intf1,a));

        then

        consider Intf1 be PartFunc of REAL , REAL such that

         A3: ( dom Intf1) = ].a, b.] and

         A4: for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,x,b)) and Intf1 is_right_convergent_in a and

         A5: y1 = ( lim_right (Intf1,a));

        assume ex Intf2 be PartFunc of REAL , REAL st ( dom Intf2) = ].a, b.] & (for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,x,b))) & Intf2 is_right_convergent_in a & y2 = ( lim_right (Intf2,a));

        then

        consider Intf2 be PartFunc of REAL , REAL such that

         A6: ( dom Intf2) = ].a, b.] and

         A7: for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,x,b)) and Intf2 is_right_convergent_in a and

         A8: y2 = ( lim_right (Intf2,a));

        now

          let x be Element of REAL ;

          assume

           A9: x in ( dom Intf1);

          

          hence (Intf1 . x) = ( integral (f,x,b)) by A4

          .= (Intf2 . x) by A3, A6, A7, A9;

        end;

        hence thesis by A3, A5, A6, A8, PARTFUN1: 5;

      end;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let a be Real;

      :: INTEGR10:def5

      pred f is_+infty_ext_Riemann_integrable_on a means (for b be Real st a <= b holds f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded) & ex Intf be PartFunc of REAL , REAL st ( dom Intf) = ( right_closed_halfline a) & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x))) & Intf is convergent_in+infty;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let b be Real;

      :: INTEGR10:def6

      pred f is_-infty_ext_Riemann_integrable_on b means (for a be Real st a <= b holds f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded) & ex Intf be PartFunc of REAL , REAL st ( dom Intf) = ( left_closed_halfline b) & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b))) & Intf is convergent_in-infty;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let a be Real;

      assume

       A1: f is_+infty_ext_Riemann_integrable_on a;

      :: INTEGR10:def7

      func infty_ext_right_integral (f,a) -> Real means

      : Def7: ex Intf be PartFunc of REAL , REAL st ( dom Intf) = ( right_closed_halfline a) & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x))) & Intf is convergent_in+infty & it = ( lim_in+infty Intf);

      existence

      proof

        consider Intf be PartFunc of REAL , REAL such that

         A2: (( dom Intf) = ( right_closed_halfline a) & for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x))) & Intf is convergent_in+infty by A1;

        take ( lim_in+infty Intf);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let L1,L2 be Real;

        assume ex Intf1 be PartFunc of REAL , REAL st ( dom Intf1) = ( right_closed_halfline a) & (for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,a,x))) & Intf1 is convergent_in+infty & L1 = ( lim_in+infty Intf1);

        then

        consider Intf1 be PartFunc of REAL , REAL such that

         A3: ( dom Intf1) = ( right_closed_halfline a) and

         A4: for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,a,x)) and Intf1 is convergent_in+infty and

         A5: L1 = ( lim_in+infty Intf1);

        assume ex Intf2 be PartFunc of REAL , REAL st ( dom Intf2) = ( right_closed_halfline a) & (for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,a,x))) & Intf2 is convergent_in+infty & L2 = ( lim_in+infty Intf2);

        then

        consider Intf2 be PartFunc of REAL , REAL such that

         A6: ( dom Intf2) = ( right_closed_halfline a) and

         A7: for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,a,x)) and Intf2 is convergent_in+infty and

         A8: L2 = ( lim_in+infty Intf2);

        now

          let x be Element of REAL ;

          assume

           A9: x in ( dom Intf1);

          

          hence (Intf1 . x) = ( integral (f,a,x)) by A4

          .= (Intf2 . x) by A3, A6, A7, A9;

        end;

        hence thesis by A3, A5, A6, A8, PARTFUN1: 5;

      end;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      let b be Real;

      assume

       A1: f is_-infty_ext_Riemann_integrable_on b;

      :: INTEGR10:def8

      func infty_ext_left_integral (f,b) -> Real means

      : Def8: ex Intf be PartFunc of REAL , REAL st ( dom Intf) = ( left_closed_halfline b) & (for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b))) & Intf is convergent_in-infty & it = ( lim_in-infty Intf);

      existence

      proof

        consider Intf be PartFunc of REAL , REAL such that

         A2: (( dom Intf) = ( left_closed_halfline b) & for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b))) & Intf is convergent_in-infty by A1;

        take ( lim_in-infty Intf);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let L1,L2 be Real;

        assume ex Intf1 be PartFunc of REAL , REAL st ( dom Intf1) = ( left_closed_halfline b) & (for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,x,b))) & Intf1 is convergent_in-infty & L1 = ( lim_in-infty Intf1);

        then

        consider Intf1 be PartFunc of REAL , REAL such that

         A3: ( dom Intf1) = ( left_closed_halfline b) and

         A4: for x be Real st x in ( dom Intf1) holds (Intf1 . x) = ( integral (f,x,b)) and Intf1 is convergent_in-infty and

         A5: L1 = ( lim_in-infty Intf1);

        assume ex Intf2 be PartFunc of REAL , REAL st ( dom Intf2) = ( left_closed_halfline b) & (for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,x,b))) & Intf2 is convergent_in-infty & L2 = ( lim_in-infty Intf2);

        then

        consider Intf2 be PartFunc of REAL , REAL such that

         A6: ( dom Intf2) = ( left_closed_halfline b) and

         A7: for x be Real st x in ( dom Intf2) holds (Intf2 . x) = ( integral (f,x,b)) and Intf2 is convergent_in-infty and

         A8: L2 = ( lim_in-infty Intf2);

        now

          let x be Element of REAL ;

          assume

           A9: x in ( dom Intf1);

          

          hence (Intf1 . x) = ( integral (f,x,b)) by A4

          .= (Intf2 . x) by A3, A6, A7, A9;

        end;

        hence thesis by A3, A5, A6, A8, PARTFUN1: 5;

      end;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      :: INTEGR10:def9

      attr f is infty_ext_Riemann_integrable means f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      :: INTEGR10:def10

      func infty_ext_integral (f) -> Real equals (( infty_ext_right_integral (f, 0 )) + ( infty_ext_left_integral (f, 0 )));

      coherence ;

    end

    begin

    theorem :: INTEGR10:4

    for f,g be PartFunc of REAL , REAL , a,b be Real st a < b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & f is_right_ext_Riemann_integrable_on (a,b) & g is_right_ext_Riemann_integrable_on (a,b) holds (f + g) is_right_ext_Riemann_integrable_on (a,b) & ( ext_right_integral ((f + g),a,b)) = (( ext_right_integral (f,a,b)) + ( ext_right_integral (g,a,b)))

    proof

      let f,g be PartFunc of REAL , REAL , a,b be Real such that

       A1: a < b and

       A2: ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) and

       A3: f is_right_ext_Riemann_integrable_on (a,b) and

       A4: g is_right_ext_Riemann_integrable_on (a,b);

      consider Intg be PartFunc of REAL , REAL such that

       A5: ( dom Intg) = [.a, b.[ and

       A6: for x be Real st x in ( dom Intg) holds (Intg . x) = ( integral (g,a,x)) and

       A7: Intg is_left_convergent_in b and

       A8: ( ext_right_integral (g,a,b)) = ( lim_left (Intg,b)) by A4, Def3;

      consider Intf be PartFunc of REAL , REAL such that

       A9: ( dom Intf) = [.a, b.[ and

       A10: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x)) and

       A11: Intf is_left_convergent_in b and

       A12: ( ext_right_integral (f,a,b)) = ( lim_left (Intf,b)) by A3, Def3;

      set Intfg = (Intf + Intg);

      

       A13: ( dom Intfg) = [.a, b.[ & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((f + g),a,x))

      proof

        

         A14: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

        

        thus

         A15: ( dom Intfg) = (( dom Intf) /\ ( dom Intg)) by VALUED_1:def 1

        .= [.a, b.[ by A9, A5;

        let x be Real;

        assume

         A16: x in ( dom Intfg);

        then

         A17: x < b by A15, XXREAL_1: 3;

        then

         A18: [.a, x.] c= [.a, b.] by XXREAL_1: 34;

        

         A19: a <= x by A15, A16, XXREAL_1: 3;

        then

         A20: f is_integrable_on ['a, x'] & (f | ['a, x']) is bounded by A3, A17;

         ['a, x'] = [.a, x.] by A19, INTEGRA5:def 3;

        then

         A21: ['a, x'] c= ( dom f) & ['a, x'] c= ( dom g) by A2, A14, A18;

        

         A22: g is_integrable_on ['a, x'] & (g | ['a, x']) is bounded by A4, A19, A17;

        

        thus (Intfg . x) = ((Intf . x) + (Intg . x)) by A16, VALUED_1:def 1

        .= (( integral (f,a,x)) + (Intg . x)) by A9, A10, A15, A16

        .= (( integral (f,a,x)) + ( integral (g,a,x))) by A5, A6, A15, A16

        .= ( integral ((f + g),a,x)) by A19, A21, A20, A22, INTEGRA6: 12;

      end;

      

       A23: for r st r < b holds ex g st r < g & g < b & g in ( dom (Intf + Intg))

      proof

        let r be Real such that

         A24: r < b;

        per cases ;

          suppose

           A25: r < a;

          reconsider g = a as Real;

          take g;

          thus thesis by A1, A13, A25, XXREAL_1: 3;

        end;

          suppose not r < a;

          then

           A26: (a - a) <= (r - a) by XREAL_1: 9;

          reconsider g = (r + ((b - r) / 2)) as Real;

          take g;

          

           A27: 0 < (b - r) by A24, XREAL_1: 50;

          then ((b - r) / 2) < (b - r) by XREAL_1: 216;

          then

           A28: (((b - r) / 2) + r) < ((b - r) + r) by XREAL_1: 8;

          r < g by A27, XREAL_1: 29, XREAL_1: 215;

          then

           A29: (r - (r - a)) < (g - 0 ) by A26, XREAL_1: 14;

           0 < ((b - r) / 2) by A27, XREAL_1: 215;

          hence thesis by A13, A29, A28, XREAL_1: 8, XXREAL_1: 3;

        end;

      end;

      then

       A30: Intfg is_left_convergent_in b by A11, A7, LIMFUNC2: 45;

      for d be Real st a <= d & d < b holds (f + g) is_integrable_on ['a, d'] & ((f + g) | ['a, d']) is bounded

      proof

        let d be Real;

        assume

         A31: a <= d & d < b;

        then

         A32: ['a, d'] = [.a, d.] & [.a, d.] c= [.a, b.] by INTEGRA5:def 3, XXREAL_1: 34;

         ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

        then

         A33: ['a, d'] c= ( dom f) & ['a, d'] c= ( dom g) by A2, A32;

        

         A34: f is_integrable_on ['a, d'] & g is_integrable_on ['a, d'] by A3, A4, A31;

        

         A35: (f | ['a, d']) is bounded & (g | ['a, d']) is bounded by A3, A4, A31;

        then ((f + g) | ( ['a, d'] /\ ['a, d'])) is bounded by RFUNCT_1: 83;

        hence thesis by A33, A34, A35, INTEGRA6: 11;

      end;

      hence

       A36: (f + g) is_right_ext_Riemann_integrable_on (a,b) by A13, A30;

      ( lim_left (Intfg,b)) = (( ext_right_integral (f,a,b)) + ( ext_right_integral (g,a,b))) by A11, A12, A7, A8, A23, LIMFUNC2: 45;

      hence thesis by A13, A30, A36, Def3;

    end;

    theorem :: INTEGR10:5

    for f be PartFunc of REAL , REAL , a,b be Real st a < b & ['a, b'] c= ( dom f) & f is_right_ext_Riemann_integrable_on (a,b) holds for r be Real holds (r (#) f) is_right_ext_Riemann_integrable_on (a,b) & ( ext_right_integral ((r (#) f),a,b)) = (r * ( ext_right_integral (f,a,b)))

    proof

      let f be PartFunc of REAL , REAL , a,b be Real such that

       A1: a < b and

       A2: ['a, b'] c= ( dom f) and

       A3: f is_right_ext_Riemann_integrable_on (a,b);

      for r be Real holds (r (#) f) is_right_ext_Riemann_integrable_on (a,b) & ( ext_right_integral ((r (#) f),a,b)) = (r * ( ext_right_integral (f,a,b)))

      proof

        let r be Real;

        consider Intf be PartFunc of REAL , REAL such that

         A4: ( dom Intf) = [.a, b.[ and

         A5: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x)) and

         A6: Intf is_left_convergent_in b and

         A7: ( ext_right_integral (f,a,b)) = ( lim_left (Intf,b)) by A3, Def3;

        set Intfg = (r (#) Intf);

        

         A8: Intfg is_left_convergent_in b by A6, LIMFUNC2: 43;

        

         A9: ( dom Intfg) = [.a, b.[ & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((r (#) f),a,x))

        proof

          

           A10: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

          thus

           A11: ( dom Intfg) = [.a, b.[ by A4, VALUED_1:def 5;

          let x be Real;

          assume

           A12: x in ( dom Intfg);

          then

           A13: a <= x by A11, XXREAL_1: 3;

          then

           A14: ['a, x'] = [.a, x.] by INTEGRA5:def 3;

          

           A15: x < b by A11, A12, XXREAL_1: 3;

          then

           A16: [.a, x.] c= [.a, b.] by XXREAL_1: 34;

          

           A17: f is_integrable_on ['a, x'] & (f | ['a, x']) is bounded by A3, A13, A15;

          

          thus (Intfg . x) = (r * (Intf . x)) by A12, VALUED_1:def 5

          .= (r * ( integral (f,a,x))) by A4, A5, A11, A12

          .= ( integral ((r (#) f),a,x)) by A2, A13, A14, A10, A16, A17, INTEGRA6: 10, XBOOLE_1: 1;

        end;

        for d be Real st a <= d & d < b holds (r (#) f) is_integrable_on ['a, d'] & ((r (#) f) | ['a, d']) is bounded

        proof

          let d be Real;

          assume

           A18: a <= d & d < b;

          then

           A19: ['a, d'] = [.a, d.] & [.a, d.] c= [.a, b.] by INTEGRA5:def 3, XXREAL_1: 34;

          

           A20: f is_integrable_on ['a, d'] & (f | ['a, d']) is bounded by A3, A18;

           ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

          then ['a, d'] c= ( dom f) by A2, A19;

          hence thesis by A20, INTEGRA6: 9, RFUNCT_1: 80;

        end;

        hence

         A21: (r (#) f) is_right_ext_Riemann_integrable_on (a,b) by A9, A8;

        ( lim_left (Intfg,b)) = (r * ( ext_right_integral (f,a,b))) by A6, A7, LIMFUNC2: 43;

        hence thesis by A9, A8, A21, Def3;

      end;

      hence thesis;

    end;

    theorem :: INTEGR10:6

    for f,g be PartFunc of REAL , REAL , a,b be Real st a < b & ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) & f is_left_ext_Riemann_integrable_on (a,b) & g is_left_ext_Riemann_integrable_on (a,b) holds (f + g) is_left_ext_Riemann_integrable_on (a,b) & ( ext_left_integral ((f + g),a,b)) = (( ext_left_integral (f,a,b)) + ( ext_left_integral (g,a,b)))

    proof

      let f,g be PartFunc of REAL , REAL , a,b be Real such that

       A1: a < b and

       A2: ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) and

       A3: f is_left_ext_Riemann_integrable_on (a,b) and

       A4: g is_left_ext_Riemann_integrable_on (a,b);

      consider Intg be PartFunc of REAL , REAL such that

       A5: ( dom Intg) = ].a, b.] and

       A6: for x be Real st x in ( dom Intg) holds (Intg . x) = ( integral (g,x,b)) and

       A7: Intg is_right_convergent_in a and

       A8: ( ext_left_integral (g,a,b)) = ( lim_right (Intg,a)) by A4, Def4;

      consider Intf be PartFunc of REAL , REAL such that

       A9: ( dom Intf) = ].a, b.] and

       A10: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b)) and

       A11: Intf is_right_convergent_in a and

       A12: ( ext_left_integral (f,a,b)) = ( lim_right (Intf,a)) by A3, Def4;

      set Intfg = (Intf + Intg);

      

       A13: ( dom Intfg) = ].a, b.] & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((f + g),x,b))

      proof

        

         A14: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

        

        thus

         A15: ( dom Intfg) = (( dom Intf) /\ ( dom Intg)) by VALUED_1:def 1

        .= ].a, b.] by A9, A5;

        let x be Real;

        assume

         A16: x in ( dom Intfg);

        then

         A17: a < x by A15, XXREAL_1: 2;

        then

         A18: [.x, b.] c= [.a, b.] by XXREAL_1: 34;

        

         A19: x <= b by A15, A16, XXREAL_1: 2;

        then

         A20: f is_integrable_on ['x, b'] & (f | ['x, b']) is bounded by A3, A17;

         ['x, b'] = [.x, b.] by A19, INTEGRA5:def 3;

        then

         A21: ['x, b'] c= ( dom f) & ['x, b'] c= ( dom g) by A2, A14, A18;

        

         A22: g is_integrable_on ['x, b'] & (g | ['x, b']) is bounded by A4, A17, A19;

        

        thus (Intfg . x) = ((Intf . x) + (Intg . x)) by A16, VALUED_1:def 1

        .= (( integral (f,x,b)) + (Intg . x)) by A9, A10, A15, A16

        .= (( integral (f,x,b)) + ( integral (g,x,b))) by A5, A6, A15, A16

        .= ( integral ((f + g),x,b)) by A19, A21, A20, A22, INTEGRA6: 12;

      end;

      

       A23: for r st a < r holds ex g st g < r & a < g & g in ( dom (Intf + Intg))

      proof

        let r be Real such that

         A24: a < r;

        per cases ;

          suppose

           A25: b < r;

          reconsider g = b as Real;

          take g;

          thus thesis by A1, A13, A25, XXREAL_1: 2;

        end;

          suppose

           A26: not b < r;

          reconsider g = (r - ((r - a) / 2)) as Real;

          take g;

          

           A27: 0 < (r - a) by A24, XREAL_1: 50;

          then ((r - a) / 2) < (r - a) by XREAL_1: 216;

          then

           A28: (((r - a) / 2) + (a - ((r - a) / 2))) < ((r - a) + (a - ((r - a) / 2))) by XREAL_1: 8;

          

           A29: 0 < ((r - a) / 2) by A27, XREAL_1: 215;

          then (r - ((r - a) / 2)) < (b - 0 ) by A26, XREAL_1: 15;

          hence thesis by A13, A29, A28, XREAL_1: 44, XXREAL_1: 2;

        end;

      end;

      then

       A30: Intfg is_right_convergent_in a by A11, A7, LIMFUNC2: 54;

      for d be Real st a < d & d <= b holds (f + g) is_integrable_on ['d, b'] & ((f + g) | ['d, b']) is bounded

      proof

        let d be Real;

        assume

         A31: a < d & d <= b;

        then

         A32: ['d, b'] = [.d, b.] & [.d, b.] c= [.a, b.] by INTEGRA5:def 3, XXREAL_1: 34;

         ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

        then

         A33: ['d, b'] c= ( dom f) & ['d, b'] c= ( dom g) by A2, A32;

        

         A34: f is_integrable_on ['d, b'] & g is_integrable_on ['d, b'] by A3, A4, A31;

        

         A35: (f | ['d, b']) is bounded & (g | ['d, b']) is bounded by A3, A4, A31;

        then ((f + g) | ( ['d, b'] /\ ['d, b'])) is bounded by RFUNCT_1: 83;

        hence thesis by A33, A34, A35, INTEGRA6: 11;

      end;

      hence

       A36: (f + g) is_left_ext_Riemann_integrable_on (a,b) by A13, A30;

      ( lim_right (Intfg,a)) = (( ext_left_integral (f,a,b)) + ( ext_left_integral (g,a,b))) by A11, A12, A7, A8, A23, LIMFUNC2: 54;

      hence thesis by A13, A30, A36, Def4;

    end;

    theorem :: INTEGR10:7

    for f be PartFunc of REAL , REAL , a,b be Real st a < b & ['a, b'] c= ( dom f) & f is_left_ext_Riemann_integrable_on (a,b) holds for r be Real holds (r (#) f) is_left_ext_Riemann_integrable_on (a,b) & ( ext_left_integral ((r (#) f),a,b)) = (r * ( ext_left_integral (f,a,b)))

    proof

      let f be PartFunc of REAL , REAL , a,b be Real such that

       A1: a < b and

       A2: ['a, b'] c= ( dom f) and

       A3: f is_left_ext_Riemann_integrable_on (a,b);

      for r be Real holds (r (#) f) is_left_ext_Riemann_integrable_on (a,b) & ( ext_left_integral ((r (#) f),a,b)) = (r * ( ext_left_integral (f,a,b)))

      proof

        let r be Real;

        consider Intf be PartFunc of REAL , REAL such that

         A4: ( dom Intf) = ].a, b.] and

         A5: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b)) and

         A6: Intf is_right_convergent_in a and

         A7: ( ext_left_integral (f,a,b)) = ( lim_right (Intf,a)) by A3, Def4;

        set Intfg = (r (#) Intf);

        

         A8: Intfg is_right_convergent_in a by A6, LIMFUNC2: 52;

        

         A9: ( dom Intfg) = ].a, b.] & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((r (#) f),x,b))

        proof

          

           A10: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

          thus

           A11: ( dom Intfg) = ].a, b.] by A4, VALUED_1:def 5;

          let x be Real;

          assume

           A12: x in ( dom Intfg);

          then

           A13: a < x by A11, XXREAL_1: 2;

          then

           A14: [.x, b.] c= [.a, b.] by XXREAL_1: 34;

          

           A15: x <= b by A11, A12, XXREAL_1: 2;

          then

           A16: ['x, b'] = [.x, b.] by INTEGRA5:def 3;

          

           A17: f is_integrable_on ['x, b'] & (f | ['x, b']) is bounded by A3, A13, A15;

          

          thus (Intfg . x) = (r * (Intf . x)) by A12, VALUED_1:def 5

          .= (r * ( integral (f,x,b))) by A4, A5, A11, A12

          .= ( integral ((r (#) f),x,b)) by A2, A15, A16, A10, A14, A17, INTEGRA6: 10, XBOOLE_1: 1;

        end;

        for d be Real st a < d & d <= b holds (r (#) f) is_integrable_on ['d, b'] & ((r (#) f) | ['d, b']) is bounded

        proof

          let d be Real;

          assume

           A18: a < d & d <= b;

          then

           A19: ['d, b'] = [.d, b.] & [.d, b.] c= [.a, b.] by INTEGRA5:def 3, XXREAL_1: 34;

          

           A20: f is_integrable_on ['d, b'] & (f | ['d, b']) is bounded by A3, A18;

           ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

          then ['d, b'] c= ( dom f) by A2, A19;

          hence thesis by A20, INTEGRA6: 9, RFUNCT_1: 80;

        end;

        hence

         A21: (r (#) f) is_left_ext_Riemann_integrable_on (a,b) by A9, A8;

        ( lim_right (Intfg,a)) = (r * ( ext_left_integral (f,a,b))) by A6, A7, LIMFUNC2: 52;

        hence thesis by A9, A8, A21, Def4;

      end;

      hence thesis;

    end;

    theorem :: INTEGR10:8

    

     Th8: for f,g be PartFunc of REAL , REAL , a be Real st ( right_closed_halfline a) c= ( dom f) & ( right_closed_halfline a) c= ( dom g) & f is_+infty_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a holds (f + g) is_+infty_ext_Riemann_integrable_on a & ( infty_ext_right_integral ((f + g),a)) = (( infty_ext_right_integral (f,a)) + ( infty_ext_right_integral (g,a)))

    proof

      let f,g be PartFunc of REAL , REAL , a be Real;

      assume that

       A1: ( right_closed_halfline a) c= ( dom f) & ( right_closed_halfline a) c= ( dom g) and

       A2: f is_+infty_ext_Riemann_integrable_on a and

       A3: g is_+infty_ext_Riemann_integrable_on a;

      consider Intg be PartFunc of REAL , REAL such that

       A4: ( dom Intg) = ( right_closed_halfline a) and

       A5: for x be Real st x in ( dom Intg) holds (Intg . x) = ( integral (g,a,x)) and

       A6: Intg is convergent_in+infty and

       A7: ( infty_ext_right_integral (g,a)) = ( lim_in+infty Intg) by A3, Def7;

      consider Intf be PartFunc of REAL , REAL such that

       A8: ( dom Intf) = ( right_closed_halfline a) and

       A9: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x)) and

       A10: Intf is convergent_in+infty and

       A11: ( infty_ext_right_integral (f,a)) = ( lim_in+infty Intf) by A2, Def7;

      set Intfg = (Intf + Intg);

      

       A12: ( dom Intfg) = ( right_closed_halfline a) & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((f + g),a,x))

      proof

        

        thus

         A13: ( dom Intfg) = (( dom Intf) /\ ( dom Intg)) by VALUED_1:def 1

        .= ( right_closed_halfline a) by A8, A4;

        let x be Real;

        assume

         A14: x in ( dom Intfg);

        then

         A15: a <= x by A13, XXREAL_1: 236;

        then

         A16: f is_integrable_on ['a, x'] & (f | ['a, x']) is bounded by A2;

        

         A17: [.a, x.] c= ( right_closed_halfline a) by XXREAL_1: 251;

         ['a, x'] = [.a, x.] by A15, INTEGRA5:def 3;

        then

         A18: ['a, x'] c= ( dom f) & ['a, x'] c= ( dom g) by A1, A17;

        

         A19: g is_integrable_on ['a, x'] & (g | ['a, x']) is bounded by A3, A15;

        

        thus (Intfg . x) = ((Intf . x) + (Intg . x)) by A14, VALUED_1:def 1

        .= (( integral (f,a,x)) + (Intg . x)) by A8, A9, A13, A14

        .= (( integral (f,a,x)) + ( integral (g,a,x))) by A4, A5, A13, A14

        .= ( integral ((f + g),a,x)) by A15, A18, A16, A19, INTEGRA6: 12;

      end;

      

       A20: for r holds ex g st r < g & g in ( dom (Intf + Intg))

      proof

        let r be Real;

        per cases ;

          suppose

           A21: r < a;

          reconsider g = a as Real;

          take g;

          thus thesis by A12, A21, XXREAL_1: 236;

        end;

          suppose

           A22: not r < a;

          reconsider g = (r + 1) as Real;

          take g;

          

           A23: (r + 0 ) < (r + 1) by XREAL_1: 8;

          then a <= g by A22, XXREAL_0: 2;

          hence thesis by A12, A23, XXREAL_1: 236;

        end;

      end;

      then

       A24: Intfg is convergent_in+infty by A10, A6, LIMFUNC1: 82;

      for b be Real st a <= b holds (f + g) is_integrable_on ['a, b'] & ((f + g) | ['a, b']) is bounded

      proof

        let b be Real;

        

         A25: [.a, b.] c= ( right_closed_halfline a) by XXREAL_1: 251;

        assume

         A26: a <= b;

        then

         A27: f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] by A2, A3;

         ['a, b'] = [.a, b.] by A26, INTEGRA5:def 3;

        then

         A28: ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) by A1, A25;

        

         A29: (f | ['a, b']) is bounded & (g | ['a, b']) is bounded by A2, A3, A26;

        then ((f + g) | ( ['a, b'] /\ ['a, b'])) is bounded by RFUNCT_1: 83;

        hence thesis by A28, A27, A29, INTEGRA6: 11;

      end;

      hence

       A30: (f + g) is_+infty_ext_Riemann_integrable_on a by A12, A24;

      ( lim_in+infty Intfg) = (( infty_ext_right_integral (f,a)) + ( infty_ext_right_integral (g,a))) by A10, A11, A6, A7, A20, LIMFUNC1: 82;

      hence thesis by A12, A24, A30, Def7;

    end;

    theorem :: INTEGR10:9

    

     Th9: for f be PartFunc of REAL , REAL , a be Real st ( right_closed_halfline a) c= ( dom f) & f is_+infty_ext_Riemann_integrable_on a holds for r be Real holds (r (#) f) is_+infty_ext_Riemann_integrable_on a & ( infty_ext_right_integral ((r (#) f),a)) = (r * ( infty_ext_right_integral (f,a)))

    proof

      let f be PartFunc of REAL , REAL , a be Real;

      assume that

       A1: ( right_closed_halfline a) c= ( dom f) and

       A2: f is_+infty_ext_Riemann_integrable_on a;

      for r be Real holds (r (#) f) is_+infty_ext_Riemann_integrable_on a & ( infty_ext_right_integral ((r (#) f),a)) = (r * ( infty_ext_right_integral (f,a)))

      proof

        let r be Real;

        consider Intf be PartFunc of REAL , REAL such that

         A3: ( dom Intf) = ( right_closed_halfline a) and

         A4: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x)) and

         A5: Intf is convergent_in+infty and

         A6: ( infty_ext_right_integral (f,a)) = ( lim_in+infty Intf) by A2, Def7;

        set Intfg = (r (#) Intf);

        

         A7: Intfg is convergent_in+infty by A5, LIMFUNC1: 80;

        

         A8: ( dom Intfg) = ( right_closed_halfline a) & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((r (#) f),a,x))

        proof

          thus

           A9: ( dom Intfg) = ( right_closed_halfline a) by A3, VALUED_1:def 5;

          let x be Real;

          assume

           A10: x in ( dom Intfg);

          then

           A11: a <= x by A9, XXREAL_1: 236;

          then

           A12: ['a, x'] = [.a, x.] & f is_integrable_on ['a, x'] by A2, INTEGRA5:def 3;

          

           A13: [.a, x.] c= ( right_closed_halfline a) & (f | ['a, x']) is bounded by A2, A11, XXREAL_1: 251;

          

          thus (Intfg . x) = (r * (Intf . x)) by A10, VALUED_1:def 5

          .= (r * ( integral (f,a,x))) by A3, A4, A9, A10

          .= ( integral ((r (#) f),a,x)) by A1, A11, A12, A13, INTEGRA6: 10, XBOOLE_1: 1;

        end;

        for b be Real st a <= b holds (r (#) f) is_integrable_on ['a, b'] & ((r (#) f) | ['a, b']) is bounded

        proof

          let b be Real;

          

           A14: [.a, b.] c= ( right_closed_halfline a) by XXREAL_1: 251;

          assume

           A15: a <= b;

          then

           A16: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded by A2;

           ['a, b'] = [.a, b.] by A15, INTEGRA5:def 3;

          then ['a, b'] c= ( dom f) by A1, A14;

          hence thesis by A16, INTEGRA6: 9, RFUNCT_1: 80;

        end;

        hence

         A17: (r (#) f) is_+infty_ext_Riemann_integrable_on a by A8, A7;

        ( lim_in+infty Intfg) = (r * ( infty_ext_right_integral (f,a))) by A5, A6, LIMFUNC1: 80;

        hence thesis by A8, A7, A17, Def7;

      end;

      hence thesis;

    end;

    theorem :: INTEGR10:10

    for f,g be PartFunc of REAL , REAL , b be Real st ( left_closed_halfline b) c= ( dom f) & ( left_closed_halfline b) c= ( dom g) & f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b holds (f + g) is_-infty_ext_Riemann_integrable_on b & ( infty_ext_left_integral ((f + g),b)) = (( infty_ext_left_integral (f,b)) + ( infty_ext_left_integral (g,b)))

    proof

      let f,g be PartFunc of REAL , REAL , b be Real;

      assume that

       A1: ( left_closed_halfline b) c= ( dom f) & ( left_closed_halfline b) c= ( dom g) and

       A2: f is_-infty_ext_Riemann_integrable_on b and

       A3: g is_-infty_ext_Riemann_integrable_on b;

      consider Intg be PartFunc of REAL , REAL such that

       A4: ( dom Intg) = ( left_closed_halfline b) and

       A5: for x be Real st x in ( dom Intg) holds (Intg . x) = ( integral (g,x,b)) and

       A6: Intg is convergent_in-infty and

       A7: ( infty_ext_left_integral (g,b)) = ( lim_in-infty Intg) by A3, Def8;

      consider Intf be PartFunc of REAL , REAL such that

       A8: ( dom Intf) = ( left_closed_halfline b) and

       A9: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b)) and

       A10: Intf is convergent_in-infty and

       A11: ( infty_ext_left_integral (f,b)) = ( lim_in-infty Intf) by A2, Def8;

      set Intfg = (Intf + Intg);

      

       A12: ( dom Intfg) = ( left_closed_halfline b) & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((f + g),x,b))

      proof

        

        thus

         A13: ( dom Intfg) = (( dom Intf) /\ ( dom Intg)) by VALUED_1:def 1

        .= ( left_closed_halfline b) by A8, A4;

        let x be Real;

        assume

         A14: x in ( dom Intfg);

        then

         A15: x <= b by A13, XXREAL_1: 234;

        then

         A16: f is_integrable_on ['x, b'] & (f | ['x, b']) is bounded by A2;

        

         A17: [.x, b.] c= ( left_closed_halfline b) by XXREAL_1: 265;

         ['x, b'] = [.x, b.] by A15, INTEGRA5:def 3;

        then

         A18: ['x, b'] c= ( dom f) & ['x, b'] c= ( dom g) by A1, A17;

        

         A19: g is_integrable_on ['x, b'] & (g | ['x, b']) is bounded by A3, A15;

        

        thus (Intfg . x) = ((Intf . x) + (Intg . x)) by A14, VALUED_1:def 1

        .= (( integral (f,x,b)) + (Intg . x)) by A8, A9, A13, A14

        .= (( integral (f,x,b)) + ( integral (g,x,b))) by A4, A5, A13, A14

        .= ( integral ((f + g),x,b)) by A15, A18, A16, A19, INTEGRA6: 12;

      end;

      

       A20: for r holds ex g st g < r & g in ( dom (Intf + Intg))

      proof

        let r be Real;

        per cases ;

          suppose

           A21: b < r;

          reconsider g = b as Real;

          take g;

          thus thesis by A12, A21, XXREAL_1: 234;

        end;

          suppose

           A22: not b < r;

          reconsider g = (r - 1) as Real;

          take g;

          

           A23: (r - 1) < (r - 0 ) by XREAL_1: 15;

          then g <= b by A22, XXREAL_0: 2;

          hence thesis by A12, A23, XXREAL_1: 234;

        end;

      end;

      then

       A24: Intfg is convergent_in-infty by A10, A6, LIMFUNC1: 91;

      for a be Real st a <= b holds (f + g) is_integrable_on ['a, b'] & ((f + g) | ['a, b']) is bounded

      proof

        let a be Real;

        

         A25: [.a, b.] c= ( left_closed_halfline b) by XXREAL_1: 265;

        assume

         A26: a <= b;

        then

         A27: f is_integrable_on ['a, b'] & g is_integrable_on ['a, b'] by A2, A3;

         ['a, b'] = [.a, b.] by A26, INTEGRA5:def 3;

        then

         A28: ['a, b'] c= ( dom f) & ['a, b'] c= ( dom g) by A1, A25;

        

         A29: (f | ['a, b']) is bounded & (g | ['a, b']) is bounded by A2, A3, A26;

        then ((f + g) | ( ['a, b'] /\ ['a, b'])) is bounded by RFUNCT_1: 83;

        hence thesis by A28, A27, A29, INTEGRA6: 11;

      end;

      hence

       A30: (f + g) is_-infty_ext_Riemann_integrable_on b by A12, A24;

      ( lim_in-infty Intfg) = (( infty_ext_left_integral (f,b)) + ( infty_ext_left_integral (g,b))) by A10, A11, A6, A7, A20, LIMFUNC1: 91;

      hence thesis by A12, A24, A30, Def8;

    end;

    theorem :: INTEGR10:11

    for f be PartFunc of REAL , REAL , b be Real st ( left_closed_halfline b) c= ( dom f) & f is_-infty_ext_Riemann_integrable_on b holds for r be Real holds (r (#) f) is_-infty_ext_Riemann_integrable_on b & ( infty_ext_left_integral ((r (#) f),b)) = (r * ( infty_ext_left_integral (f,b)))

    proof

      let f be PartFunc of REAL , REAL , b be Real;

      assume that

       A1: ( left_closed_halfline b) c= ( dom f) and

       A2: f is_-infty_ext_Riemann_integrable_on b;

      for r be Real holds (r (#) f) is_-infty_ext_Riemann_integrable_on b & ( infty_ext_left_integral ((r (#) f),b)) = (r * ( infty_ext_left_integral (f,b)))

      proof

        let r be Real;

        consider Intf be PartFunc of REAL , REAL such that

         A3: ( dom Intf) = ( left_closed_halfline b) and

         A4: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b)) and

         A5: Intf is convergent_in-infty and

         A6: ( infty_ext_left_integral (f,b)) = ( lim_in-infty Intf) by A2, Def8;

        set Intfg = (r (#) Intf);

        

         A7: Intfg is convergent_in-infty by A5, LIMFUNC1: 89;

        

         A8: ( dom Intfg) = ( left_closed_halfline b) & for x be Real st x in ( dom Intfg) holds (Intfg . x) = ( integral ((r (#) f),x,b))

        proof

          thus

           A9: ( dom Intfg) = ( left_closed_halfline b) by A3, VALUED_1:def 5;

          let x be Real;

          assume

           A10: x in ( dom Intfg);

          then

           A11: x <= b by A9, XXREAL_1: 234;

          then

           A12: ['x, b'] = [.x, b.] & f is_integrable_on ['x, b'] by A2, INTEGRA5:def 3;

          

           A13: [.x, b.] c= ( left_closed_halfline b) & (f | ['x, b']) is bounded by A2, A11, XXREAL_1: 265;

          

          thus (Intfg . x) = (r * (Intf . x)) by A10, VALUED_1:def 5

          .= (r * ( integral (f,x,b))) by A3, A4, A9, A10

          .= ( integral ((r (#) f),x,b)) by A1, A11, A12, A13, INTEGRA6: 10, XBOOLE_1: 1;

        end;

        for a be Real st a <= b holds (r (#) f) is_integrable_on ['a, b'] & ((r (#) f) | ['a, b']) is bounded

        proof

          let a be Real;

          

           A14: [.a, b.] c= ( left_closed_halfline b) by XXREAL_1: 265;

          assume

           A15: a <= b;

          then

           A16: f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded by A2;

           ['a, b'] = [.a, b.] by A15, INTEGRA5:def 3;

          then ['a, b'] c= ( dom f) by A1, A14;

          hence thesis by A16, INTEGRA6: 9, RFUNCT_1: 80;

        end;

        hence

         A17: (r (#) f) is_-infty_ext_Riemann_integrable_on b by A8, A7;

        ( lim_in-infty Intfg) = (r * ( infty_ext_left_integral (f,b))) by A5, A6, LIMFUNC1: 89;

        hence thesis by A8, A7, A17, Def8;

      end;

      hence thesis;

    end;

    theorem :: INTEGR10:12

    for f be PartFunc of REAL , REAL , a,b be Real st a < b & ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded holds ( ext_right_integral (f,a,b)) = ( integral (f,a,b))

    proof

      let f be PartFunc of REAL , REAL , a,b be Real such that

       A1: a < b and

       A2: ['a, b'] c= ( dom f) and

       A3: f is_integrable_on ['a, b'] and

       A4: (f | ['a, b']) is bounded;

      reconsider AB = [.a, b.[ as non empty Subset of REAL by A1, XXREAL_1: 3;

      deffunc F( Element of AB) = ( In (( integral (f,a,$1)), REAL ));

      consider Intf be Function of AB, REAL such that

       A5: for x be Element of AB holds (Intf . x) = F(x) from FUNCT_2:sch 4;

      

       A6: ( dom Intf) = AB by FUNCT_2:def 1;

      then

      reconsider Intf as PartFunc of REAL , REAL by RELSET_1: 5;

      consider M0 be Real such that

       A7: for x be object st x in ( ['a, b'] /\ ( dom f)) holds |.(f . x).| <= M0 by A4, RFUNCT_1: 73;

      reconsider M = (M0 + 1) as Real;

      

       A8: for x be Real st x in ['a, b'] holds |.(f . x).| < M

      proof

        

         A9: ( ['a, b'] /\ ( dom f)) = ['a, b'] by A2, XBOOLE_1: 28;

        let x be Real;

        assume x in ['a, b'];

        hence thesis by A7, A9, XREAL_1: 39;

      end;

      a in { r where r be Real : a <= r & r <= b } by A1;

      then a in [.a, b.] by RCOMP_1:def 1;

      then a in ['a, b'] by A1, INTEGRA5:def 3;

      then |.(f . a).| < M by A8;

      then

       A10: 0 < M by COMPLEX1: 46;

      

       A11: for g1 be Real st 0 < g1 holds ex r be Real st r < b & for r1 be Real st r < r1 & r1 < b & r1 in ( dom Intf) holds |.((Intf . r1) - ( integral (f,a,b))).| < g1

      proof

        let g1 be Real;

        assume 0 < g1;

        then

        consider r be Real such that

         A12: a < r and

         A13: r < b and

         A14: ((b - r) * M) < g1 by A1, A10, Th1;

        reconsider r as Real;

        take r;

        thus r < b by A13;

        now

          let r1 be Real;

          assume that

           A15: r < r1 and

           A16: r1 < b and r1 in ( dom Intf);

          

           A17: a <= r1 by A12, A15, XXREAL_0: 2;

          then

          reconsider rr = r1 as Element of AB by A16, XXREAL_1: 3;

          

           A18: (Intf . r1) = F(rr) by A5;

          r1 in [.a, b.] by A16, XXREAL_1: 1, A17;

          then

           A19: r1 in ['a, b'] by A1, INTEGRA5:def 3;

          (b - r1) < (b - r) by A15, XREAL_1: 15;

          then

           A20: (M * (b - r1)) < (M * (b - r)) by A10, XREAL_1: 68;

          

           A21: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

           [.r1, b.] = ['r1, b'] by A16, INTEGRA5:def 3;

          then ['r1, b'] c= ['a, b'] by A21, A17, XXREAL_1: 34;

          then

           A22: for x be Real st x in ['r1, b'] holds |.(f . x).| <= M by A8;

          b in ['a, b'] by A1, A21, XXREAL_1: 1;

          then |.( integral (f,r1,b)).| <= (M * (b - r1)) by A1, A2, A3, A4, A16, A19, A22, INTEGRA6: 23;

          then

           A23: |.( integral (f,r1,b)).| < (M * (b - r)) by A20, XXREAL_0: 2;

           |.((Intf . r1) - ( integral (f,a,b))).| = |.(( integral (f,a,b)) - (Intf . r1)).| by COMPLEX1: 60

          .= |.((( integral (f,a,r1)) + ( integral (f,r1,b))) - ( integral (f,a,r1))).| by A1, A2, A3, A4, A18, A19, INTEGRA6: 17

          .= |.( integral (f,r1,b)).|;

          hence |.((Intf . r1) - ( integral (f,a,b))).| < g1 by A14, A23, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      

       A24: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,a,x))

      proof

        let x be Real such that

         A25: x in ( dom Intf);

        ( dom Intf) = AB by FUNCT_2:def 1;

        then

        reconsider x as Element of AB by A25;

        (Intf . x) = F(x) by A5;

        hence thesis;

      end;

      for r st r < b holds ex g be Real st r < g & g < b & g in ( dom Intf)

      proof

        let r such that

         A26: r < b;

        per cases ;

          suppose

           A27: r < a;

          reconsider g = a as Real;

          take g;

          thus thesis by A1, A6, A27, XXREAL_1: 3;

        end;

          suppose not r < a;

          then

           A28: (a - a) <= (r - a) by XREAL_1: 9;

          reconsider g = (r + ((b - r) / 2)) as Real;

          take g;

          

           A29: 0 < (b - r) by A26, XREAL_1: 50;

          then ((b - r) / 2) < (b - r) by XREAL_1: 216;

          then

           A30: (((b - r) / 2) + r) < ((b - r) + r) by XREAL_1: 8;

          r < g by A29, XREAL_1: 29, XREAL_1: 215;

          then

           A31: (r - (r - a)) < (g - 0 ) by A28, XREAL_1: 14;

           0 < ((b - r) / 2) by A29, XREAL_1: 215;

          hence thesis by A6, A31, A30, XREAL_1: 8, XXREAL_1: 3;

        end;

      end;

      then

       A32: Intf is_left_convergent_in b by A11, LIMFUNC2: 7;

      then

       A33: ( integral (f,a,b)) = ( lim_left (Intf,b)) by A11, LIMFUNC2: 41;

      for d be Real st a <= d & d < b holds f is_integrable_on ['a, d'] & (f | ['a, d']) is bounded by A2, A3, A4, INTEGRA6: 18;

      then f is_right_ext_Riemann_integrable_on (a,b) by A6, A24, A32;

      hence thesis by A6, A24, A32, A33, Def3;

    end;

    theorem :: INTEGR10:13

    for f be PartFunc of REAL , REAL , a,b be Real st a < b & ['a, b'] c= ( dom f) & f is_integrable_on ['a, b'] & (f | ['a, b']) is bounded holds ( ext_left_integral (f,a,b)) = ( integral (f,a,b))

    proof

      let f be PartFunc of REAL , REAL , a,b be Real such that

       A1: a < b and

       A2: ['a, b'] c= ( dom f) and

       A3: f is_integrable_on ['a, b'] and

       A4: (f | ['a, b']) is bounded;

      reconsider AB = ].a, b.] as non empty Subset of REAL by A1, XXREAL_1: 2;

      deffunc F( Element of AB) = ( In (( integral (f,$1,b)), REAL ));

      consider Intf be Function of AB, REAL such that

       A5: for x be Element of AB holds (Intf . x) = F(x) from FUNCT_2:sch 4;

      

       A6: ( dom Intf) = AB by FUNCT_2:def 1;

      then

      reconsider Intf as PartFunc of REAL , REAL by RELSET_1: 5;

      consider M0 be Real such that

       A7: for x be object st x in ( ['a, b'] /\ ( dom f)) holds |.(f . x).| <= M0 by A4, RFUNCT_1: 73;

      reconsider M = (M0 + 1) as Real;

      

       A8: for x be Real st x in ['a, b'] holds |.(f . x).| < M

      proof

        

         A9: ( ['a, b'] /\ ( dom f)) = ['a, b'] by A2, XBOOLE_1: 28;

        let x be Real;

        assume x in ['a, b'];

        hence thesis by A7, A9, XREAL_1: 39;

      end;

      a in { r where r be Real : a <= r & r <= b } by A1;

      then a in [.a, b.] by RCOMP_1:def 1;

      then a in ['a, b'] by A1, INTEGRA5:def 3;

      then |.(f . a).| < M by A8;

      then

       A10: 0 < M by COMPLEX1: 46;

      

       A11: for g1 be Real st 0 < g1 holds ex r be Real st a < r & for r1 be Real st r1 < r & a < r1 & r1 in ( dom Intf) holds |.((Intf . r1) - ( integral (f,a,b))).| < g1

      proof

        let g1 be Real;

        assume 0 < g1;

        then

        consider r be Real such that

         A12: a < r and

         A13: r < b and

         A14: ((r - a) * M) < g1 by A1, A10, Th2;

        take r;

        thus a < r by A12;

        now

          let r1 be Real;

          assume that

           A15: a < r1 and

           A16: r1 < r and r1 in ( dom Intf);

          r1 < b by A16, A13, XXREAL_0: 2;

          then

          reconsider rr = r1 as Element of AB by A15, XXREAL_1: 2;

          

           A17: (Intf . r1) = F(rr) by A5;

          (r1 - a) < (r - a) by A16, XREAL_1: 14;

          then

           A18: (M * (r1 - a)) < (M * (r - a)) by A10, XREAL_1: 68;

          

           A19: ['a, b'] = [.a, b.] by A1, INTEGRA5:def 3;

          

           A20: r1 <= b by A13, A16, XXREAL_0: 2;

          then

           A21: r1 in ['a, b'] by A15, A19, XXREAL_1: 1;

           [.a, r1.] = ['a, r1'] by A15, INTEGRA5:def 3;

          then ['a, r1'] c= ['a, b'] by A19, A20, XXREAL_1: 34;

          then

           A22: for x be Real st x in ['a, r1'] holds |.(f . x).| <= M by A8;

          a in ['a, b'] by A1, A19, XXREAL_1: 1;

          then |.( integral (f,a,r1)).| <= (M * (r1 - a)) by A1, A2, A3, A4, A15, A21, A22, INTEGRA6: 23;

          then

           A23: |.( integral (f,a,r1)).| < (M * (r - a)) by A18, XXREAL_0: 2;

           |.((Intf . r1) - ( integral (f,a,b))).| = |.(( integral (f,a,b)) - (Intf . r1)).| by COMPLEX1: 60

          .= |.((( integral (f,a,r1)) + ( integral (f,r1,b))) - ( integral (f,r1,b))).| by A1, A2, A3, A4, A17, A21, INTEGRA6: 17

          .= |.( integral (f,a,r1)).|;

          hence |.((Intf . r1) - ( integral (f,a,b))).| < g1 by A14, A23, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      

       A24: for x be Real st x in ( dom Intf) holds (Intf . x) = ( integral (f,x,b))

      proof

        let x be Real such that

         A25: x in ( dom Intf);

        ( dom Intf) = AB by FUNCT_2:def 1;

        then

        reconsider x as Element of AB by A25;

        (Intf . x) = F(x) by A5;

        hence thesis;

      end;

      for r st a < r holds ex g be Real st g < r & a < g & g in ( dom Intf)

      proof

        let r such that

         A26: a < r;

        per cases ;

          suppose

           A27: b < r;

          reconsider g = b as Real;

          take g;

          g in ].a, b.] by A1, XXREAL_1: 2;

          hence thesis by A1, A27, FUNCT_2:def 1;

        end;

          suppose

           A28: not b < r;

          reconsider g = (a + ((r - a) / 2)) as Real;

          take g;

          

           A29: 0 < (r - a) by A26, XREAL_1: 50;

          then

           A30: a < g by XREAL_1: 29, XREAL_1: 215;

          ((r - a) / 2) < (r - a) by A29, XREAL_1: 216;

          then

           A31: (((r - a) / 2) + a) < ((r - a) + a) by XREAL_1: 8;

          then g < b by A28, XXREAL_0: 2;

          hence thesis by A6, A30, A31, XXREAL_1: 2;

        end;

      end;

      then

       A32: Intf is_right_convergent_in a by A11, LIMFUNC2: 10;

      then

       A33: ( integral (f,a,b)) = ( lim_right (Intf,a)) by A11, LIMFUNC2: 42;

      for d be Real st a < d & d <= b holds f is_integrable_on ['d, b'] & (f | ['d, b']) is bounded by A2, A3, A4, INTEGRA6: 18;

      then f is_left_ext_Riemann_integrable_on (a,b) by A6, A24, A32;

      hence thesis by A6, A24, A32, A33, Def4;

    end;

    begin

    definition

      let s be Real;

      :: INTEGR10:def11

      func exp*- s -> Function of REAL , REAL means for t be Real holds (it . t) = ( exp_R . ( - (s * t)));

      existence

      proof

        deffunc F( Real) = ( In (( exp_R . ( - (s * $1))), REAL ));

        consider g be Function of REAL , REAL such that

         A1: for x be Element of REAL holds (g . x) = F(x) from FUNCT_2:sch 4;

        take g;

        let x be Real;

        x in REAL by XREAL_0:def 1;

        then (g . x) = F(x) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of REAL , REAL ;

        assume that

         A2: for d be Real holds (f1 . d) = ( exp_R . ( - (s * d))) and

         A3: for d be Real holds (f2 . d) = ( exp_R . ( - (s * d)));

        for d be Element of REAL holds (f1 . d) = (f2 . d)

        proof

          let d be Element of REAL ;

          

          thus (f1 . d) = ( exp_R . ( - (s * d))) by A2

          .= (f2 . d) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      :: INTEGR10:def12

      func One-sided_Laplace_transform (f) -> PartFunc of REAL , REAL means

      : Def12: ( dom it ) = ( right_open_halfline 0 ) & for s be Real st s in ( dom it ) holds (it . s) = ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 ));

      existence

      proof

        defpred P[ Real, Real] means $1 in ( right_open_halfline 0 ) & $2 = ( infty_ext_right_integral ((f (#) ( exp*- $1)), 0 ));

        consider g be PartFunc of REAL , REAL such that

         A1: (for d be Element of REAL holds d in ( dom g) iff (ex c be Element of REAL st P[d, c])) & for d be Element of REAL st d in ( dom g) holds P[d, (g /. d)] from PARTFUN2:sch 1;

        

         A2: for d be Real holds d in ( dom g) iff ex c be Real st P[d, c]

        proof

          let d be Real;

          reconsider dd = d as Element of REAL by XREAL_0:def 1;

          thus d in ( dom g) implies ex c be Real st P[d, c] by A1;

          given c be Real such that

           A3: P[d, c];

          reconsider c as Element of REAL by XREAL_0:def 1;

           P[dd, c] by A3;

          then dd in ( dom g) by A1;

          hence thesis;

        end;

        

         A4: for d be Real st d in ( dom g) holds P[d, (g /. d)] by A1;

        

         A5: ( dom g) = ( right_open_halfline 0 )

        proof

          let s1 be Real;

          reconsider s = s1 as Real;

          s in ( right_open_halfline 0 ) implies s in ( dom g)

          proof

            assume s in ( right_open_halfline 0 );

            then ex y be Real st s in ( right_open_halfline 0 ) & y = ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 ));

            hence thesis by A2;

          end;

          hence thesis by A4;

        end;

        take g;

        for s be Real st s in ( dom g) holds (g . s) = ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 ))

        proof

          let s be Real;

          assume

           A6: s in ( dom g);

          then (g /. s) = ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 )) by A4;

          hence thesis by A6, PARTFUN1:def 6;

        end;

        hence thesis by A5;

      end;

      uniqueness

      proof

        let f1,f2 be PartFunc of REAL , REAL ;

        assume that

         A7: ( dom f1) = ( right_open_halfline 0 ) and

         A8: for s be Real st s in ( dom f1) holds (f1 . s) = ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 ));

        assume that

         A9: ( dom f2) = ( right_open_halfline 0 ) and

         A10: for s be Real st s in ( dom f2) holds (f2 . s) = ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 ));

        for s be Element of REAL st s in ( dom f1) holds (f1 . s) = (f2 . s)

        proof

          let s be Element of REAL such that

           A11: s in ( dom f1);

          (f1 . s) = ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 )) by A8, A11;

          hence thesis by A7, A9, A10, A11;

        end;

        hence f1 = f2 by A7, A9, PARTFUN1: 5;

      end;

    end

    begin

    theorem :: INTEGR10:14

    for f,g be PartFunc of REAL , REAL st ( dom f) = ( right_closed_halfline 0 ) & ( dom g) = ( right_closed_halfline 0 ) & (for s be Real st s in ( right_open_halfline 0 ) holds (f (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ) & (for s be Real st s in ( right_open_halfline 0 ) holds (g (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ) holds (for s be Real st s in ( right_open_halfline 0 ) holds ((f + g) (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ) & ( One-sided_Laplace_transform (f + g)) = (( One-sided_Laplace_transform f) + ( One-sided_Laplace_transform g))

    proof

      let f,g be PartFunc of REAL , REAL such that

       A1: ( dom f) = ( right_closed_halfline 0 ) and

       A2: ( dom g) = ( right_closed_halfline 0 ) and

       A3: (for s be Real st s in ( right_open_halfline 0 ) holds (f (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ) & for s be Real st s in ( right_open_halfline 0 ) holds (g (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ;

      set Intg = ( One-sided_Laplace_transform g);

      set Intf = ( One-sided_Laplace_transform f);

      set F = (( One-sided_Laplace_transform f) + ( One-sided_Laplace_transform g));

      

       A4: ( dom F) = (( dom Intf) /\ ( dom Intg)) by VALUED_1:def 1

      .= (( right_open_halfline 0 ) /\ ( dom Intg)) by Def12

      .= (( right_open_halfline 0 ) /\ ( right_open_halfline 0 )) by Def12

      .= ( right_open_halfline 0 );

      

       A5: for s be Real st s in ( right_open_halfline 0 ) holds ((f + g) (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 & ( infty_ext_right_integral (((f + g) (#) ( exp*- s)), 0 )) = (( infty_ext_right_integral ((f (#) ( exp*- s)), 0 )) + ( infty_ext_right_integral ((g (#) ( exp*- s)), 0 )))

      proof

        let s be Real;

        

         A6: ((f + g) (#) ( exp*- s)) = ((f (#) ( exp*- s)) + (g (#) ( exp*- s))) by RFUNCT_1: 10;

        

         A7: ( dom (g (#) ( exp*- s))) = (( dom g) /\ ( dom ( exp*- s))) by VALUED_1:def 4

        .= (( right_closed_halfline 0 ) /\ REAL ) by A2, FUNCT_2:def 1

        .= ( right_closed_halfline 0 ) by XBOOLE_1: 28;

        assume s in ( right_open_halfline 0 );

        then

         A8: (f (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 & (g (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 by A3;

        ( dom (f (#) ( exp*- s))) = (( dom f) /\ ( dom ( exp*- s))) by VALUED_1:def 4

        .= (( right_closed_halfline 0 ) /\ REAL ) by A1, FUNCT_2:def 1

        .= ( right_closed_halfline 0 ) by XBOOLE_1: 28;

        hence thesis by A8, A6, A7, Th8;

      end;

      for s be Real st s in ( dom F) holds (F . s) = ( infty_ext_right_integral (((f + g) (#) ( exp*- s)), 0 ))

      proof

        let s be Real;

        assume

         A9: s in ( dom F);

        then

         A10: s in ( dom Intf) by A4, Def12;

        

         A11: s in ( dom Intg) by A4, A9, Def12;

        

        thus ( infty_ext_right_integral (((f + g) (#) ( exp*- s)), 0 )) = (( infty_ext_right_integral ((f (#) ( exp*- s)), 0 )) + ( infty_ext_right_integral ((g (#) ( exp*- s)), 0 ))) by A5, A4, A9

        .= ((Intf . s) + ( infty_ext_right_integral ((g (#) ( exp*- s)), 0 ))) by A10, Def12

        .= ((Intf . s) + (Intg . s)) by A11, Def12

        .= (F . s) by A9, VALUED_1:def 1;

      end;

      hence thesis by A5, A4, Def12;

    end;

    theorem :: INTEGR10:15

    for f be PartFunc of REAL , REAL , a be Real st ( dom f) = ( right_closed_halfline 0 ) & (for s be Real st s in ( right_open_halfline 0 ) holds (f (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ) holds (for s be Real st s in ( right_open_halfline 0 ) holds ((a (#) f) (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ) & ( One-sided_Laplace_transform (a (#) f)) = (a (#) ( One-sided_Laplace_transform f))

    proof

      let f be PartFunc of REAL , REAL , a be Real such that

       A1: ( dom f) = ( right_closed_halfline 0 ) and

       A2: for s be Real st s in ( right_open_halfline 0 ) holds (f (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 ;

      set Intf = ( One-sided_Laplace_transform f);

      set F = (a (#) ( One-sided_Laplace_transform f));

      

       A3: ( dom F) = ( dom Intf) by VALUED_1:def 5

      .= ( right_open_halfline 0 ) by Def12;

      

       A4: for s be Real st s in ( right_open_halfline 0 ) holds ((a (#) f) (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 & ( infty_ext_right_integral (((a (#) f) (#) ( exp*- s)), 0 )) = (a * ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 )))

      proof

        let s be Real;

        

         A5: ((a (#) f) (#) ( exp*- s)) = (a (#) (f (#) ( exp*- s))) by RFUNCT_1: 12;

        assume s in ( right_open_halfline 0 );

        then

         A6: (f (#) ( exp*- s)) is_+infty_ext_Riemann_integrable_on 0 by A2;

        ( dom (f (#) ( exp*- s))) = (( dom f) /\ ( dom ( exp*- s))) by VALUED_1:def 4

        .= (( right_closed_halfline 0 ) /\ REAL ) by A1, FUNCT_2:def 1

        .= ( right_closed_halfline 0 ) by XBOOLE_1: 28;

        hence thesis by A6, A5, Th9;

      end;

      for s be Real st s in ( dom F) holds (F . s) = ( infty_ext_right_integral (((a (#) f) (#) ( exp*- s)), 0 ))

      proof

        let s be Real;

        assume

         A7: s in ( dom F);

        then

         A8: s in ( dom Intf) by A3, Def12;

        

        thus ( infty_ext_right_integral (((a (#) f) (#) ( exp*- s)), 0 )) = (a * ( infty_ext_right_integral ((f (#) ( exp*- s)), 0 ))) by A4, A3, A7

        .= (a * (Intf . s)) by A8, Def12

        .= (F . s) by VALUED_1: 6;

      end;

      hence thesis by A4, A3, Def12;

    end;