limfunc4.miz



    begin

    reserve r,r1,r2,g,g1,g2,x0 for Real;

    reserve f1,f2 for PartFunc of REAL , REAL ;

    

     Lm1: 0 < g implies (r - g) < r & r < (r + g)

    proof

      assume

       A1: 0 < g;

      then (r - g) < (r - 0 ) by XREAL_1: 15;

      hence (r - g) < r;

      (r + 0 ) < (r + g) by A1, XREAL_1: 8;

      hence thesis;

    end;

    

     Lm2: for s be Real_Sequence st ( rng s) c= ( dom (f2 * f1)) holds ( rng s) c= ( dom f1) & ( rng (f1 /* s)) c= ( dom f2)

    proof

      let s be Real_Sequence such that

       A1: ( rng s) c= ( dom (f2 * f1));

      

       A2: ( dom (f2 * f1)) c= ( dom f1) by RELAT_1: 25;

      hence ( rng s) c= ( dom f1) by A1;

      let x be object;

      assume x in ( rng (f1 /* s));

      then

      consider n be Element of NAT such that

       A3: ((f1 /* s) . n) = x by FUNCT_2: 113;

      (s . n) in ( rng s) by VALUED_0: 28;

      then (f1 . (s . n)) in ( dom f2) by A1, FUNCT_1: 11;

      hence thesis by A1, A2, A3, FUNCT_2: 108, XBOOLE_1: 1;

    end;

    theorem :: LIMFUNC4:1

    

     Th1: for s be Real_Sequence, X be set st ( rng s) c= (( dom (f2 * f1)) /\ X) holds ( rng s) c= ( dom (f2 * f1)) & ( rng s) c= X & ( rng s) c= ( dom f1) & ( rng s) c= (( dom f1) /\ X) & ( rng (f1 /* s)) c= ( dom f2)

    proof

      let s be Real_Sequence, X be set;

      assume ( rng s) c= (( dom (f2 * f1)) /\ X);

      hence

       A1: ( rng s) c= ( dom (f2 * f1)) & ( rng s) c= X by XBOOLE_1: 18;

      

       A2: ( dom (f2 * f1)) c= ( dom f1) by RELAT_1: 25;

      hence ( rng s) c= ( dom f1) by A1;

      hence ( rng s) c= (( dom f1) /\ X) by A1, XBOOLE_1: 19;

      let x be object;

      assume x in ( rng (f1 /* s));

      then

      consider n be Element of NAT such that

       A3: ((f1 /* s) . n) = x by FUNCT_2: 113;

      (s . n) in ( rng s) by VALUED_0: 28;

      then (f1 . (s . n)) in ( dom f2) by A1, FUNCT_1: 11;

      hence thesis by A1, A2, A3, FUNCT_2: 108, XBOOLE_1: 1;

    end;

    theorem :: LIMFUNC4:2

    

     Th2: for s be Real_Sequence, X be set st ( rng s) c= (( dom (f2 * f1)) \ X) holds ( rng s) c= ( dom (f2 * f1)) & ( rng s) c= ( dom f1) & ( rng s) c= (( dom f1) \ X) & ( rng (f1 /* s)) c= ( dom f2)

    proof

      let s be Real_Sequence, X be set such that

       A1: ( rng s) c= (( dom (f2 * f1)) \ X);

      (( dom (f2 * f1)) \ X) c= ( dom (f2 * f1)) by XBOOLE_1: 36;

      hence

       A2: ( rng s) c= ( dom (f2 * f1)) by A1;

      

       A3: ( dom (f2 * f1)) c= ( dom f1) by RELAT_1: 25;

      hence

       A4: ( rng s) c= ( dom f1) by A2;

      thus ( rng s) c= (( dom f1) \ X)

      proof

        let x be object;

        assume

         A5: x in ( rng s);

        then not x in X by A1, XBOOLE_0:def 5;

        hence thesis by A4, A5, XBOOLE_0:def 5;

      end;

      let x be object;

      assume x in ( rng (f1 /* s));

      then

      consider n be Element of NAT such that

       A6: ((f1 /* s) . n) = x by FUNCT_2: 113;

      (s . n) in ( rng s) by VALUED_0: 28;

      then (f1 . (s . n)) in ( dom f2) by A2, FUNCT_1: 11;

      hence thesis by A2, A3, A6, FUNCT_2: 108, XBOOLE_1: 1;

    end;

    theorem :: LIMFUNC4:3

    f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & (for r holds ex g st r < g & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to+infty and

       A2: f2 is divergent_in+infty_to+infty and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to+infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to+infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to+infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:4

    f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to-infty & (for r holds ex g st r < g & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in+infty_to-infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to+infty and

       A2: f2 is divergent_in+infty_to-infty and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to+infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to+infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to-infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:5

    f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to+infty & (for r holds ex g st r < g & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to-infty and

       A2: f2 is divergent_in-infty_to+infty and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to+infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to-infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to+infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:6

    f1 is divergent_in+infty_to-infty & f2 is divergent_in-infty_to-infty & (for r holds ex g st r < g & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in+infty_to-infty

    proof

      assume that

       A1: f1 is divergent_in+infty_to-infty and

       A2: f2 is divergent_in-infty_to-infty and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to+infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to-infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to-infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:7

    f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to+infty & (for r holds ex g st g < r & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to+infty and

       A2: f2 is divergent_in+infty_to+infty and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to-infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to+infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to+infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:8

    f1 is divergent_in-infty_to+infty & f2 is divergent_in+infty_to-infty & (for r holds ex g st g < r & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in-infty_to-infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to+infty and

       A2: f2 is divergent_in+infty_to-infty and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to-infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to+infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to-infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:9

    f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to+infty & (for r holds ex g st g < r & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to-infty and

       A2: f2 is divergent_in-infty_to+infty and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to-infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to-infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to+infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:10

    f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & (for r holds ex g st g < r & g in ( dom (f2 * f1))) implies (f2 * f1) is divergent_in-infty_to-infty

    proof

      assume that

       A1: f1 is divergent_in-infty_to-infty and

       A2: f2 is divergent_in-infty_to-infty and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is divergent_to-infty and

         A5: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A5, Lm2;

        then

         A6: (f1 /* s) is divergent_to-infty by A1, A4;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Lm2;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A6;

        hence ((f2 * f1) /* s) is divergent_to-infty by A5, VALUED_0: 31;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:11

    f1 is_left_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) implies (f2 * f1) is_left_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_left_divergent_to+infty_in x0 and

       A2: f2 is divergent_in+infty_to+infty and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A4, LIMFUNC2:def 2;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to+infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 2;

    end;

    theorem :: LIMFUNC4:12

    f1 is_left_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) implies (f2 * f1) is_left_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_left_divergent_to+infty_in x0 and

       A2: f2 is divergent_in+infty_to-infty and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A4, LIMFUNC2:def 2;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to-infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 3;

    end;

    theorem :: LIMFUNC4:13

    f1 is_left_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) implies (f2 * f1) is_left_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_left_divergent_to-infty_in x0 and

       A2: f2 is divergent_in-infty_to+infty and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A4, LIMFUNC2:def 3;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to+infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 2;

    end;

    theorem :: LIMFUNC4:14

    f1 is_left_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) implies (f2 * f1) is_left_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_left_divergent_to-infty_in x0 and

       A2: f2 is divergent_in-infty_to-infty and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A4, LIMFUNC2:def 3;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to-infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 3;

    end;

    theorem :: LIMFUNC4:15

    f1 is_right_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) implies (f2 * f1) is_right_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_right_divergent_to+infty_in x0 and

       A2: f2 is divergent_in+infty_to+infty and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A4, LIMFUNC2:def 5;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to+infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 5;

    end;

    theorem :: LIMFUNC4:16

    f1 is_right_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) implies (f2 * f1) is_right_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_right_divergent_to+infty_in x0 and

       A2: f2 is divergent_in+infty_to-infty and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A4, LIMFUNC2:def 5;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to-infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 6;

    end;

    theorem :: LIMFUNC4:17

    f1 is_right_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) implies (f2 * f1) is_right_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_right_divergent_to-infty_in x0 and

       A2: f2 is divergent_in-infty_to+infty and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A4, LIMFUNC2:def 6;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to+infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 5;

    end;

    theorem :: LIMFUNC4:18

    f1 is_right_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) implies (f2 * f1) is_right_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_right_divergent_to-infty_in x0 and

       A2: f2 is divergent_in-infty_to-infty and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th1;

        ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A5, Th1;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A4, LIMFUNC2:def 6;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th1;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to-infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC2:def 6;

    end;

    theorem :: LIMFUNC4:19

    f1 is_left_convergent_in x0 & f2 is_left_divergent_to+infty_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) < ( lim_left (f1,x0))) implies (f2 * f1) is_left_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_left_divergent_to+infty_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) < ( lim_left (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A6, Lm1, LIMFUNC2: 1;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 7;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( left_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (x0 - g) < (s . (n + k)) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A18;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_left (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { r1 : r1 < ( lim_left (f1,x0)) };

          then

           A20: (f1 . (s . (n + k))) in ( left_open_halfline ( lim_left (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim_left (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim_left (f1,x0))));

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A6, A11, LIMFUNC2:def 7;

        then ( lim q) = ( lim_left (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A21, LIMFUNC2:def 2;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 2;

    end;

    theorem :: LIMFUNC4:20

    f1 is_left_convergent_in x0 & f2 is_left_divergent_to-infty_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) < ( lim_left (f1,x0))) implies (f2 * f1) is_left_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_left_divergent_to-infty_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) < ( lim_left (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A6, Lm1, LIMFUNC2: 1;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 7;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( left_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (x0 - g) < (s . (n + k)) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A18;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_left (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { r1 : r1 < ( lim_left (f1,x0)) };

          then

           A20: (f1 . (s . (n + k))) in ( left_open_halfline ( lim_left (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim_left (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim_left (f1,x0))));

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A6, A11, LIMFUNC2:def 7;

        then ( lim q) = ( lim_left (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A21, LIMFUNC2:def 3;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 3;

    end;

    theorem :: LIMFUNC4:21

    f1 is_left_convergent_in x0 & f2 is_right_divergent_to+infty_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds ( lim_left (f1,x0)) < (f1 . r)) implies (f2 * f1) is_left_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_right_divergent_to+infty_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds ( lim_left (f1,x0)) < (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A6, Lm1, LIMFUNC2: 1;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 7;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( left_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (x0 - g) < (s . (n + k)) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A18;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A13, A19, XBOOLE_0:def 4;

          then ( lim_left (f1,x0)) < (f1 . (s . (n + k))) by A5;

          then (f1 . (s . (n + k))) in { r1 : ( lim_left (f1,x0)) < r1 };

          then

           A20: (f1 . (s . (n + k))) in ( right_open_halfline ( lim_left (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim_left (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim_left (f1,x0))));

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A6, A11, LIMFUNC2:def 7;

        then ( lim q) = ( lim_left (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A21, LIMFUNC2:def 5;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 2;

    end;

    theorem :: LIMFUNC4:22

    f1 is_left_convergent_in x0 & f2 is_right_divergent_to-infty_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds ( lim_left (f1,x0)) < (f1 . r)) implies (f2 * f1) is_left_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_right_divergent_to-infty_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds ( lim_left (f1,x0)) < (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A6, Lm1, LIMFUNC2: 1;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 7;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( left_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (x0 - g) < (s . (n + k)) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A18;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A13, A19, XBOOLE_0:def 4;

          then ( lim_left (f1,x0)) < (f1 . (s . (n + k))) by A5;

          then (f1 . (s . (n + k))) in { r1 : ( lim_left (f1,x0)) < r1 };

          then

           A20: (f1 . (s . (n + k))) in ( right_open_halfline ( lim_left (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim_left (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim_left (f1,x0))));

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A6, A11, LIMFUNC2:def 7;

        then ( lim q) = ( lim_left (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A21, LIMFUNC2:def 6;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 3;

    end;

    theorem :: LIMFUNC4:23

    f1 is_right_convergent_in x0 & f2 is_right_divergent_to+infty_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds ( lim_right (f1,x0)) < (f1 . r)) implies (f2 * f1) is_right_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_right_divergent_to+infty_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds ( lim_right (f1,x0)) < (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A6, Lm1, LIMFUNC2: 2;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 8;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( right_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (s . (n + k)) < (x0 + g) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A18;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A13, A19, XBOOLE_0:def 4;

          then ( lim_right (f1,x0)) < (f1 . (s . (n + k))) by A5;

          then (f1 . (s . (n + k))) in { r1 : ( lim_right (f1,x0)) < r1 };

          then

           A20: (f1 . (s . (n + k))) in ( right_open_halfline ( lim_right (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim_right (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim_right (f1,x0))));

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A6, A11, LIMFUNC2:def 8;

        then ( lim q) = ( lim_right (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A21, LIMFUNC2:def 5;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 5;

    end;

    theorem :: LIMFUNC4:24

    f1 is_right_convergent_in x0 & f2 is_right_divergent_to-infty_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds ( lim_right (f1,x0)) < (f1 . r)) implies (f2 * f1) is_right_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_right_divergent_to-infty_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds ( lim_right (f1,x0)) < (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A6, Lm1, LIMFUNC2: 2;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 8;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( right_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (s . (n + k)) < (x0 + g) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A18;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A13, A19, XBOOLE_0:def 4;

          then ( lim_right (f1,x0)) < (f1 . (s . (n + k))) by A5;

          then (f1 . (s . (n + k))) in { r1 : ( lim_right (f1,x0)) < r1 };

          then

           A20: (f1 . (s . (n + k))) in ( right_open_halfline ( lim_right (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim_right (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim_right (f1,x0))));

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A6, A11, LIMFUNC2:def 8;

        then ( lim q) = ( lim_right (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A21, LIMFUNC2:def 6;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 6;

    end;

    theorem :: LIMFUNC4:25

    f1 is_right_convergent_in x0 & f2 is_left_divergent_to+infty_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) < ( lim_right (f1,x0))) implies (f2 * f1) is_right_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_left_divergent_to+infty_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) < ( lim_right (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A6, Lm1, LIMFUNC2: 2;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 8;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( right_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (s . (n + k)) < (x0 + g) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A18;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_right (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { r1 : r1 < ( lim_right (f1,x0)) };

          then

           A20: (f1 . (s . (n + k))) in ( left_open_halfline ( lim_right (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim_right (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim_right (f1,x0))));

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A6, A11, LIMFUNC2:def 8;

        then ( lim q) = ( lim_right (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A21, LIMFUNC2:def 2;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 5;

    end;

    theorem :: LIMFUNC4:26

    f1 is_right_convergent_in x0 & f2 is_left_divergent_to-infty_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) < ( lim_right (f1,x0))) implies (f2 * f1) is_right_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_left_divergent_to-infty_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) < ( lim_right (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A6, Lm1, LIMFUNC2: 2;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 8;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( right_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (s . (n + k)) < (x0 + g) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A18;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_right (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { r1 : r1 < ( lim_right (f1,x0)) };

          then

           A20: (f1 . (s . (n + k))) in ( left_open_halfline ( lim_right (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim_right (f1,x0)))) by A20, A17, XBOOLE_0:def 4;

        end;

        then

         A21: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim_right (f1,x0))));

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A6, A11, LIMFUNC2:def 8;

        then ( lim q) = ( lim_right (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A21, LIMFUNC2:def 3;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 6;

    end;

    theorem :: LIMFUNC4:27

    f1 is convergent_in+infty & f2 is_left_divergent_to+infty_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) < ( lim_in+infty f1)) implies (f2 * f1) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_left_divergent_to+infty_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) < ( lim_in+infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds r < (s . n) by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A5, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( left_open_halfline ( lim_in+infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A15: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_in+infty f1) by A4;

          then x in { g1 : g1 < ( lim_in+infty f1) } by A14;

          then

           A16: x in ( left_open_halfline ( lim_in+infty f1)) by XXREAL_1: 229;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to+infty by A2, A12, LIMFUNC2:def 2;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to+infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:28

    f1 is convergent_in+infty & f2 is_left_divergent_to-infty_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) < ( lim_in+infty f1)) implies (f2 * f1) is divergent_in+infty_to-infty

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_left_divergent_to-infty_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) < ( lim_in+infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds r < (s . n) by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A5, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( left_open_halfline ( lim_in+infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A15: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_in+infty f1) by A4;

          then x in { g1 : g1 < ( lim_in+infty f1) } by A14;

          then

           A16: x in ( left_open_halfline ( lim_in+infty f1)) by XXREAL_1: 229;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to-infty by A2, A12, LIMFUNC2:def 3;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to-infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:29

    f1 is convergent_in+infty & f2 is_right_divergent_to+infty_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds ( lim_in+infty f1) < (f1 . g)) implies (f2 * f1) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_right_divergent_to+infty_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds ( lim_in+infty f1) < (f1 . g);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds r < (s . n) by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A5, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( right_open_halfline ( lim_in+infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A15: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then ( lim_in+infty f1) < (f1 . (s . (n + k))) by A4;

          then x in { g1 : ( lim_in+infty f1) < g1 } by A14;

          then

           A16: x in ( right_open_halfline ( lim_in+infty f1)) by XXREAL_1: 230;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to+infty by A2, A12, LIMFUNC2:def 5;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to+infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:30

    f1 is convergent_in+infty & f2 is_right_divergent_to-infty_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds ( lim_in+infty f1) < (f1 . g)) implies (f2 * f1) is divergent_in+infty_to-infty

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_right_divergent_to-infty_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds ( lim_in+infty f1) < (f1 . g);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds r < (s . n) by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A5, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( right_open_halfline ( lim_in+infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A15: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then ( lim_in+infty f1) < (f1 . (s . (n + k))) by A4;

          then x in { g1 : ( lim_in+infty f1) < g1 } by A14;

          then

           A16: x in ( right_open_halfline ( lim_in+infty f1)) by XXREAL_1: 230;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to-infty by A2, A12, LIMFUNC2:def 6;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to-infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:31

    f1 is convergent_in-infty & f2 is_left_divergent_to+infty_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) < ( lim_in-infty f1)) implies (f2 * f1) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_left_divergent_to+infty_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) < ( lim_in-infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds (s . n) < r by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A5, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( left_open_halfline ( lim_in-infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A15: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_in-infty f1) by A4;

          then x in { g1 : g1 < ( lim_in-infty f1) } by A14;

          then

           A16: x in ( left_open_halfline ( lim_in-infty f1)) by XXREAL_1: 229;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to+infty by A2, A12, LIMFUNC2:def 2;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to+infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:32

    f1 is convergent_in-infty & f2 is_left_divergent_to-infty_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) < ( lim_in-infty f1)) implies (f2 * f1) is divergent_in-infty_to-infty

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_left_divergent_to-infty_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) < ( lim_in-infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds (s . n) < r by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A5, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( left_open_halfline ( lim_in-infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A15: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_in-infty f1) by A4;

          then x in { g1 : g1 < ( lim_in-infty f1) } by A14;

          then

           A16: x in ( left_open_halfline ( lim_in-infty f1)) by XXREAL_1: 229;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to-infty by A2, A12, LIMFUNC2:def 3;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to-infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:33

    f1 is convergent_in-infty & f2 is_right_divergent_to+infty_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds ( lim_in-infty f1) < (f1 . g)) implies (f2 * f1) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_right_divergent_to+infty_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds ( lim_in-infty f1) < (f1 . g);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds (s . n) < r by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A5, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( right_open_halfline ( lim_in-infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A15: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then ( lim_in-infty f1) < (f1 . (s . (n + k))) by A4;

          then x in { g1 : ( lim_in-infty f1) < g1 } by A14;

          then

           A16: x in ( right_open_halfline ( lim_in-infty f1)) by XXREAL_1: 230;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to+infty by A2, A12, LIMFUNC2:def 5;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to+infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:34

    f1 is convergent_in-infty & f2 is_right_divergent_to-infty_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds ( lim_in-infty f1) < (f1 . g)) implies (f2 * f1) is divergent_in-infty_to-infty

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_right_divergent_to-infty_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds ( lim_in-infty f1) < (f1 . g);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds (s . n) < r by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A5, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) /\ ( right_open_halfline ( lim_in-infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A15: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then ( lim_in-infty f1) < (f1 . (s . (n + k))) by A4;

          then x in { g1 : ( lim_in-infty f1) < g1 } by A14;

          then

           A16: x in ( right_open_halfline ( lim_in-infty f1)) by XXREAL_1: 230;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A16, XBOOLE_0:def 4;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to-infty by A2, A12, LIMFUNC2:def 6;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to-infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:35

    f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to+infty & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) implies (f2 * f1) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to+infty_in x0 and

       A2: f2 is divergent_in+infty_to+infty and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th2;

        ( rng s) c= (( dom f1) \ {x0}) by A5, Th2;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A4, LIMFUNC3:def 2;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th2;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to+infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC3:def 2;

    end;

    theorem :: LIMFUNC4:36

    f1 is_divergent_to+infty_in x0 & f2 is divergent_in+infty_to-infty & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) implies (f2 * f1) is_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to+infty_in x0 and

       A2: f2 is divergent_in+infty_to-infty and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th2;

        ( rng s) c= (( dom f1) \ {x0}) by A5, Th2;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A4, LIMFUNC3:def 2;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th2;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to-infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC3:def 3;

    end;

    theorem :: LIMFUNC4:37

    f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to+infty & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) implies (f2 * f1) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to-infty_in x0 and

       A2: f2 is divergent_in-infty_to+infty and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th2;

        ( rng s) c= (( dom f1) \ {x0}) by A5, Th2;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A4, LIMFUNC3:def 3;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th2;

        then (f2 /* (f1 /* s)) is divergent_to+infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to+infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC3:def 2;

    end;

    theorem :: LIMFUNC4:38

    f1 is_divergent_to-infty_in x0 & f2 is divergent_in-infty_to-infty & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) implies (f2 * f1) is_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_divergent_to-infty_in x0 and

       A2: f2 is divergent_in-infty_to-infty and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      now

        let s be Real_Sequence;

        assume that

         A4: s is convergent & ( lim s) = x0 and

         A5: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        

         A6: ( rng s) c= ( dom (f2 * f1)) by A5, Th2;

        ( rng s) c= (( dom f1) \ {x0}) by A5, Th2;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A4, LIMFUNC3:def 3;

        ( rng (f1 /* s)) c= ( dom f2) by A5, Th2;

        then (f2 /* (f1 /* s)) is divergent_to-infty by A2, A7;

        hence ((f2 * f1) /* s) is divergent_to-infty by A6, VALUED_0: 31;

      end;

      hence thesis by A3, LIMFUNC3:def 3;

    end;

    theorem :: LIMFUNC4:39

    f1 is_convergent_in x0 & f2 is_divergent_to+infty_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) <> ( lim (f1,x0))) implies (f2 * f1) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_divergent_to+infty_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) <> ( lim (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A8: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A6, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th2;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th2;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) \ {x0}) by A7, Th2;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC3:def 4;

        

         A13: ( rng s) c= ( dom f1) by A7, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A14: (q . n) = x by FUNCT_2: 113;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108

          .= x by A14, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A8;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A16: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A7, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A16, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A13, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim (f1,x0)) by A5;

          then

           A18: not (f1 . (s . (n + k))) in {( lim (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A17, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim (f1,x0))}) by A18, A15, XBOOLE_0:def 5;

        end;

        then

         A19: ( rng q) c= (( dom f2) \ {( lim (f1,x0))});

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A6, A11, LIMFUNC3:def 4;

        then ( lim q) = ( lim (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A19, LIMFUNC3:def 2;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC3:def 2;

    end;

    theorem :: LIMFUNC4:40

    f1 is_convergent_in x0 & f2 is_divergent_to-infty_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) <> ( lim (f1,x0))) implies (f2 * f1) is_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_divergent_to-infty_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) <> ( lim (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A8: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A6, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th2;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th2;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) \ {x0}) by A7, Th2;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC3:def 4;

        

         A13: ( rng s) c= ( dom f1) by A7, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A14: (q . n) = x by FUNCT_2: 113;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108

          .= x by A14, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A8;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A16: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A7, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A16, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A13, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim (f1,x0)) by A5;

          then

           A18: not (f1 . (s . (n + k))) in {( lim (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A17, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim (f1,x0))}) by A18, A15, XBOOLE_0:def 5;

        end;

        then

         A19: ( rng q) c= (( dom f2) \ {( lim (f1,x0))});

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A6, A11, LIMFUNC3:def 4;

        then ( lim q) = ( lim (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A19, LIMFUNC3:def 3;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC3:def 3;

    end;

    theorem :: LIMFUNC4:41

    f1 is_convergent_in x0 & f2 is_right_divergent_to+infty_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) > ( lim (f1,x0))) implies (f2 * f1) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_right_divergent_to+infty_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds ( lim (f1,x0)) < (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A8: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A6, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th2;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th2;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) \ {x0}) by A7, Th2;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC3:def 4;

        

         A13: ( rng s) c= ( dom f1) by A7, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A14: (q . n) = x by FUNCT_2: 113;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108

          .= x by A14, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A8;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A16: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A7, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A16, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A13, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) > ( lim (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { g2 : ( lim (f1,x0)) < g2 };

          then

           A18: (f1 . (s . (n + k))) in ( right_open_halfline ( lim (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim (f1,x0))));

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A6, A11, LIMFUNC3:def 4;

        then ( lim q) = ( lim (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A19, LIMFUNC2:def 5;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC3:def 2;

    end;

    theorem :: LIMFUNC4:42

    f1 is_convergent_in x0 & f2 is_right_divergent_to-infty_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) > ( lim (f1,x0))) implies (f2 * f1) is_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_right_divergent_to-infty_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds ( lim (f1,x0)) < (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A8: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A6, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th2;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th2;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) \ {x0}) by A7, Th2;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC3:def 4;

        

         A13: ( rng s) c= ( dom f1) by A7, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A14: (q . n) = x by FUNCT_2: 113;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108

          .= x by A14, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A8;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A16: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A7, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A16, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A13, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) > ( lim (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { g2 : ( lim (f1,x0)) < g2 };

          then

           A18: (f1 . (s . (n + k))) in ( right_open_halfline ( lim (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim (f1,x0))));

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A6, A11, LIMFUNC3:def 4;

        then ( lim q) = ( lim (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A19, LIMFUNC2:def 6;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC3:def 3;

    end;

    theorem :: LIMFUNC4:43

    f1 is_right_convergent_in x0 & f2 is_divergent_to+infty_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) <> ( lim_right (f1,x0))) implies (f2 * f1) is_right_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_divergent_to+infty_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) <> ( lim_right (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A6, Lm1, LIMFUNC2: 2;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 8;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( right_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (s . (n + k)) < (x0 + g) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A18;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_right (f1,x0)) by A5;

          then

           A20: not (f1 . (s . (n + k))) in {( lim_right (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim_right (f1,x0))}) by A20, A17, XBOOLE_0:def 5;

        end;

        then

         A21: ( rng q) c= (( dom f2) \ {( lim_right (f1,x0))});

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A6, A11, LIMFUNC2:def 8;

        then ( lim q) = ( lim_right (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A21, LIMFUNC3:def 2;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 5;

    end;

    theorem :: LIMFUNC4:44

    f1 is_right_convergent_in x0 & f2 is_divergent_to-infty_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) <> ( lim_right (f1,x0))) implies (f2 * f1) is_right_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_divergent_to-infty_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) <> ( lim_right (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A6, Lm1, LIMFUNC2: 2;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 8;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( right_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (s . (n + k)) < (x0 + g) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A18;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_right (f1,x0)) by A5;

          then

           A20: not (f1 . (s . (n + k))) in {( lim_right (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim_right (f1,x0))}) by A20, A17, XBOOLE_0:def 5;

        end;

        then

         A21: ( rng q) c= (( dom f2) \ {( lim_right (f1,x0))});

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A6, A11, LIMFUNC2:def 8;

        then ( lim q) = ( lim_right (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A21, LIMFUNC3:def 3;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 6;

    end;

    theorem :: LIMFUNC4:45

    f1 is convergent_in+infty & f2 is_divergent_to+infty_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <> ( lim_in+infty f1)) implies (f2 * f1) is divergent_in+infty_to+infty

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_divergent_to+infty_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <> ( lim_in+infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds r < (s . n) by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A5, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) \ {( lim_in+infty f1)})

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A15: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_in+infty f1) by A4;

          then

           A16: not (f1 . (s . (n + k))) in {( lim_in+infty f1)} by TARSKI:def 1;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A14, A16, XBOOLE_0:def 5;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to+infty by A2, A12, LIMFUNC3:def 2;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to+infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:46

    f1 is convergent_in+infty & f2 is_divergent_to-infty_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <> ( lim_in+infty f1)) implies (f2 * f1) is divergent_in+infty_to-infty

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_divergent_to-infty_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <> ( lim_in+infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds r < (s . n) by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A5, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) \ {( lim_in+infty f1)})

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A15: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_in+infty f1) by A4;

          then

           A16: not (f1 . (s . (n + k))) in {( lim_in+infty f1)} by TARSKI:def 1;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A14, A16, XBOOLE_0:def 5;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to-infty by A2, A12, LIMFUNC3:def 3;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to-infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:47

    f1 is convergent_in-infty & f2 is_divergent_to+infty_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <> ( lim_in-infty f1)) implies (f2 * f1) is divergent_in-infty_to+infty

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_divergent_to+infty_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <> ( lim_in-infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds (s . n) < r by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A5, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) \ {( lim_in-infty f1)})

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A15: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_in-infty f1) by A4;

          then

           A16: not (f1 . (s . (n + k))) in {( lim_in-infty f1)} by TARSKI:def 1;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A14, A16, XBOOLE_0:def 5;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to+infty by A2, A12, LIMFUNC3:def 2;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to+infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:48

    f1 is convergent_in-infty & f2 is_divergent_to-infty_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <> ( lim_in-infty f1)) implies (f2 * f1) is divergent_in-infty_to-infty

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_divergent_to-infty_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <> ( lim_in-infty f1);

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A7: for n be Nat st k <= n holds (s . n) < r by A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A5, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A6, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        

         A12: ( rng (f1 /* q)) c= (( dom f2) \ {( lim_in-infty f1)})

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A13: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A14: x = (f1 . (q . n)) by A10, A11, A13, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A7, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A15: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_in-infty f1) by A4;

          then

           A16: not (f1 . (s . (n + k))) in {( lim_in-infty f1)} by TARSKI:def 1;

          

           A17: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A8;

          then x in ( dom f2) by A10, A14, FUNCT_2: 108, A17;

          hence thesis by A14, A16, XBOOLE_0:def 5;

        end;

        ( rng q) c= ( dom f1) by A10, A11;

        then (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        then

         A18: (f2 /* (f1 /* q)) is divergent_to-infty by A2, A12, LIMFUNC3:def 3;

        (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A8, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A6, VALUED_0: 31;

        hence ((f2 * f1) /* s) is divergent_to-infty by A18, LIMFUNC1: 7;

      end;

      hence thesis by A3;

    end;

    theorem :: LIMFUNC4:49

    f1 is_convergent_in x0 & f2 is_left_divergent_to+infty_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) < ( lim (f1,x0))) implies (f2 * f1) is_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_left_divergent_to+infty_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds ( lim (f1,x0)) > (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A8: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A6, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th2;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th2;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) \ {x0}) by A7, Th2;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC3:def 4;

        

         A13: ( rng s) c= ( dom f1) by A7, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A14: (q . n) = x by FUNCT_2: 113;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108

          .= x by A14, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A8;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A16: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A7, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A16, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A13, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { g2 : g2 < ( lim (f1,x0)) };

          then

           A18: (f1 . (s . (n + k))) in ( left_open_halfline ( lim (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim (f1,x0))));

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A6, A11, LIMFUNC3:def 4;

        then ( lim q) = ( lim (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A19, LIMFUNC2:def 2;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC3:def 2;

    end;

    theorem :: LIMFUNC4:50

    f1 is_convergent_in x0 & f2 is_left_divergent_to-infty_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) < ( lim (f1,x0))) implies (f2 * f1) is_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_left_divergent_to-infty_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds ( lim (f1,x0)) > (f1 . r);

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A8: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A6, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th2;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th2;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) \ {x0}) by A7, Th2;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC3:def 4;

        

         A13: ( rng s) c= ( dom f1) by A7, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A14: (q . n) = x by FUNCT_2: 113;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108

          .= x by A14, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A8;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A16: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A7, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A16, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A13, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { g2 : g2 < ( lim (f1,x0)) };

          then

           A18: (f1 . (s . (n + k))) in ( left_open_halfline ( lim (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim (f1,x0))));

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A6, A11, LIMFUNC3:def 4;

        then ( lim q) = ( lim (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A19, LIMFUNC2:def 3;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC3:def 3;

    end;

    theorem :: LIMFUNC4:51

    f1 is_left_convergent_in x0 & f2 is_divergent_to+infty_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) <> ( lim_left (f1,x0))) implies (f2 * f1) is_left_divergent_to+infty_in x0

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_divergent_to+infty_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) <> ( lim_left (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A6, Lm1, LIMFUNC2: 1;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 7;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( left_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (x0 - g) < (s . (n + k)) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A18;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_left (f1,x0)) by A5;

          then

           A20: not (f1 . (s . (n + k))) in {( lim_left (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim_left (f1,x0))}) by A20, A17, XBOOLE_0:def 5;

        end;

        then

         A21: ( rng q) c= (( dom f2) \ {( lim_left (f1,x0))});

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A6, A11, LIMFUNC2:def 7;

        then ( lim q) = ( lim_left (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to+infty by A2, A12, A21, LIMFUNC3:def 2;

        hence ((f2 * f1) /* s) is divergent_to+infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 2;

    end;

    theorem :: LIMFUNC4:52

    f1 is_left_convergent_in x0 & f2 is_divergent_to-infty_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) <> ( lim_left (f1,x0))) implies (f2 * f1) is_left_divergent_to-infty_in x0

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_divergent_to-infty_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) <> ( lim_left (f1,x0));

      now

        let s be Real_Sequence;

        assume that

         A6: s is convergent & ( lim s) = x0 and

         A7: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A6, Lm1, LIMFUNC2: 1;

        set q = ((f1 /* s) ^\ k);

        

         A9: ( rng s) c= ( dom (f2 * f1)) by A7, Th1;

        ( rng (f1 /* s)) c= ( dom f2) by A7, Th1;

        

        then

         A10: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A9, VALUED_0: 31;

        

         A11: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A7, Th1;

        then

         A12: (f1 /* s) is convergent by A1, A2, A6, LIMFUNC2:def 7;

        

         A13: ( rng s) c= ( dom f1) by A7, Th1;

        

         A14: ( rng s) c= ( left_open_halfline x0) by A7, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A15: (q . n) = x by FUNCT_2: 113;

          

           A16: (n + k) in NAT by ORDINAL1:def 12;

          

           A17: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A13, FUNCT_2: 108, A16

          .= x by A15, NAT_1:def 3;

          

           A18: (x0 - g) < (s . (n + k)) by A8, NAT_1: 12;

          

           A19: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A14;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A18;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A13, A19, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_left (f1,x0)) by A5;

          then

           A20: not (f1 . (s . (n + k))) in {( lim_left (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A9, A19, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim_left (f1,x0))}) by A20, A17, XBOOLE_0:def 5;

        end;

        then

         A21: ( rng q) c= (( dom f2) \ {( lim_left (f1,x0))});

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A6, A11, LIMFUNC2:def 7;

        then ( lim q) = ( lim_left (f1,x0)) by A12, SEQ_4: 20;

        then (f2 /* q) is divergent_to-infty by A2, A12, A21, LIMFUNC3:def 3;

        hence ((f2 * f1) /* s) is divergent_to-infty by A10, LIMFUNC1: 7;

      end;

      hence thesis by A3, LIMFUNC2:def 3;

    end;

    theorem :: LIMFUNC4:53

    f1 is divergent_in+infty_to+infty & f2 is convergent_in+infty & (for r holds ex g st r < g & g in ( dom (f2 * f1))) implies (f2 * f1) is convergent_in+infty & ( lim_in+infty (f2 * f1)) = ( lim_in+infty f2)

    proof

      assume that

       A1: f1 is divergent_in+infty_to+infty and

       A2: f2 is convergent_in+infty and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A6, Lm2;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in+infty f2) by A2, A7, LIMFUNC1:def 12;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in+infty f2) by A6, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is convergent_in+infty by A3;

      hence thesis by A4, LIMFUNC1:def 12;

    end;

    theorem :: LIMFUNC4:54

    f1 is divergent_in+infty_to-infty & f2 is convergent_in-infty & (for r holds ex g st r < g & g in ( dom (f2 * f1))) implies (f2 * f1) is convergent_in+infty & ( lim_in+infty (f2 * f1)) = ( lim_in-infty f2)

    proof

      assume that

       A1: f1 is divergent_in+infty_to-infty and

       A2: f2 is convergent_in-infty and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to+infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A6, Lm2;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in-infty f2) by A2, A7, LIMFUNC1:def 13;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in-infty f2) by A6, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is convergent_in+infty by A3;

      hence thesis by A4, LIMFUNC1:def 12;

    end;

    theorem :: LIMFUNC4:55

    f1 is divergent_in-infty_to+infty & f2 is convergent_in+infty & (for r holds ex g st g < r & g in ( dom (f2 * f1))) implies (f2 * f1) is convergent_in-infty & ( lim_in-infty (f2 * f1)) = ( lim_in+infty f2)

    proof

      assume that

       A1: f1 is divergent_in-infty_to+infty and

       A2: f2 is convergent_in+infty and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A6, Lm2;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in+infty f2) by A2, A7, LIMFUNC1:def 12;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in+infty f2) by A6, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is convergent_in-infty by A3;

      hence thesis by A4, LIMFUNC1:def 13;

    end;

    theorem :: LIMFUNC4:56

    f1 is divergent_in-infty_to-infty & f2 is convergent_in-infty & (for r holds ex g st g < r & g in ( dom (f2 * f1))) implies (f2 * f1) is convergent_in-infty & ( lim_in-infty (f2 * f1)) = ( lim_in-infty f2)

    proof

      assume that

       A1: f1 is divergent_in-infty_to-infty and

       A2: f2 is convergent_in-infty and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is divergent_to-infty and

         A6: ( rng s) c= ( dom (f2 * f1));

        ( rng s) c= ( dom f1) by A6, Lm2;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Lm2;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in-infty f2) by A2, A7, LIMFUNC1:def 13;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in-infty f2) by A6, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is convergent_in-infty by A3;

      hence thesis by A4, LIMFUNC1:def 13;

    end;

    theorem :: LIMFUNC4:57

    f1 is_left_divergent_to+infty_in x0 & f2 is convergent_in+infty & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) implies (f2 * f1) is_left_convergent_in x0 & ( lim_left ((f2 * f1),x0)) = ( lim_in+infty f2)

    proof

      assume that

       A1: f1 is_left_divergent_to+infty_in x0 and

       A2: f2 is convergent_in+infty and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent & ( lim s) = x0 and

         A6: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A6, Th1;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A5, LIMFUNC2:def 2;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Th1;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in+infty f2) by A2, A7, LIMFUNC1:def 12;

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A6, Th1;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in+infty f2) by A10, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is_left_convergent_in x0 by A3, LIMFUNC2:def 1;

      hence thesis by A4, LIMFUNC2:def 7;

    end;

    theorem :: LIMFUNC4:58

    f1 is_left_divergent_to-infty_in x0 & f2 is convergent_in-infty & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) implies (f2 * f1) is_left_convergent_in x0 & ( lim_left ((f2 * f1),x0)) = ( lim_in-infty f2)

    proof

      assume that

       A1: f1 is_left_divergent_to-infty_in x0 and

       A2: f2 is convergent_in-infty and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent & ( lim s) = x0 and

         A6: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A6, Th1;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A5, LIMFUNC2:def 3;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Th1;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in-infty f2) by A2, A7, LIMFUNC1:def 13;

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A6, Th1;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in-infty f2) by A10, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is_left_convergent_in x0 by A3, LIMFUNC2:def 1;

      hence thesis by A4, LIMFUNC2:def 7;

    end;

    theorem :: LIMFUNC4:59

    f1 is_right_divergent_to+infty_in x0 & f2 is convergent_in+infty & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) implies (f2 * f1) is_right_convergent_in x0 & ( lim_right ((f2 * f1),x0)) = ( lim_in+infty f2)

    proof

      assume that

       A1: f1 is_right_divergent_to+infty_in x0 and

       A2: f2 is convergent_in+infty and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent & ( lim s) = x0 and

         A6: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A6, Th1;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A5, LIMFUNC2:def 5;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Th1;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in+infty f2) by A2, A7, LIMFUNC1:def 12;

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A6, Th1;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in+infty f2) by A10, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is_right_convergent_in x0 by A3, LIMFUNC2:def 4;

      hence thesis by A4, LIMFUNC2:def 8;

    end;

    theorem :: LIMFUNC4:60

    f1 is_right_divergent_to-infty_in x0 & f2 is convergent_in-infty & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) implies (f2 * f1) is_right_convergent_in x0 & ( lim_right ((f2 * f1),x0)) = ( lim_in-infty f2)

    proof

      assume that

       A1: f1 is_right_divergent_to-infty_in x0 and

       A2: f2 is convergent_in-infty and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent & ( lim s) = x0 and

         A6: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A6, Th1;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A5, LIMFUNC2:def 6;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Th1;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in-infty f2) by A2, A7, LIMFUNC1:def 13;

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A6, Th1;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in-infty f2) by A10, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is_right_convergent_in x0 by A3, LIMFUNC2:def 4;

      hence thesis by A4, LIMFUNC2:def 8;

    end;

    theorem :: LIMFUNC4:61

    f1 is_left_convergent_in x0 & f2 is_left_convergent_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) < ( lim_left (f1,x0))) implies (f2 * f1) is_left_convergent_in x0 & ( lim_left ((f2 * f1),x0)) = ( lim_left (f2,( lim_left (f1,x0))))

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_left_convergent_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) < ( lim_left (f1,x0));

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A9: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A7, Lm1, LIMFUNC2: 1;

        

         A10: ( rng s) c= ( dom f1) by A8, Th1;

        set q = ((f1 /* s) ^\ k);

        

         A11: ( rng s) c= ( dom (f2 * f1)) by A8, Th1;

        

         A12: ( rng s) c= ( left_open_halfline x0) by A8, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A13: (q . n) = x by FUNCT_2: 113;

          

           A14: (n + k) in NAT by ORDINAL1:def 12;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A10, FUNCT_2: 108, A14

          .= x by A13, NAT_1:def 3;

          

           A16: (x0 - g) < (s . (n + k)) by A9, NAT_1: 12;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A12;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A16;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_left (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { r1 : r1 < ( lim_left (f1,x0)) };

          then

           A18: (f1 . (s . (n + k))) in ( left_open_halfline ( lim_left (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A11, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim_left (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim_left (f1,x0))));

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th1;

        

        then

         A20: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A11, VALUED_0: 31;

        

         A21: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A8, Th1;

        then

         A22: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC2:def 7;

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A7, A21, LIMFUNC2:def 7;

        then

         A23: ( lim q) = ( lim_left (f1,x0)) by A22, SEQ_4: 20;

        ( lim_left (f2,( lim_left (f1,x0)))) = ( lim_left (f2,( lim_left (f1,x0))));

        then

         A24: (f2 /* q) is convergent by A2, A22, A23, A19, LIMFUNC2:def 7;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim_left (f2,( lim_left (f1,x0)))) by A2, A22, A23, A19, LIMFUNC2:def 7;

        hence ( lim ((f2 * f1) /* s)) = ( lim_left (f2,( lim_left (f1,x0)))) by A24, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is_left_convergent_in x0 by A3, LIMFUNC2:def 1;

      hence thesis by A6, LIMFUNC2:def 7;

    end;

    theorem :: LIMFUNC4:62

    f1 is_right_convergent_in x0 & f2 is_right_convergent_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds ( lim_right (f1,x0)) < (f1 . r)) implies (f2 * f1) is_right_convergent_in x0 & ( lim_right ((f2 * f1),x0)) = ( lim_right (f2,( lim_right (f1,x0))))

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_right_convergent_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds ( lim_right (f1,x0)) < (f1 . r);

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A9: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A7, Lm1, LIMFUNC2: 2;

        

         A10: ( rng s) c= ( dom f1) by A8, Th1;

        set q = ((f1 /* s) ^\ k);

        

         A11: ( rng s) c= ( dom (f2 * f1)) by A8, Th1;

        

         A12: ( rng s) c= ( right_open_halfline x0) by A8, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A13: (q . n) = x by FUNCT_2: 113;

          

           A14: (n + k) in NAT by ORDINAL1:def 12;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A10, FUNCT_2: 108, A14

          .= x by A13, NAT_1:def 3;

          

           A16: (s . (n + k)) < (x0 + g) by A9, NAT_1: 12;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A12;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A16;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A10, A17, XBOOLE_0:def 4;

          then ( lim_right (f1,x0)) < (f1 . (s . (n + k))) by A5;

          then (f1 . (s . (n + k))) in { r1 : ( lim_right (f1,x0)) < r1 };

          then

           A18: (f1 . (s . (n + k))) in ( right_open_halfline ( lim_right (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A11, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim_right (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim_right (f1,x0))));

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th1;

        

        then

         A20: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A11, VALUED_0: 31;

        

         A21: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A8, Th1;

        then

         A22: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC2:def 8;

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A7, A21, LIMFUNC2:def 8;

        then

         A23: ( lim q) = ( lim_right (f1,x0)) by A22, SEQ_4: 20;

        ( lim_right (f2,( lim_right (f1,x0)))) = ( lim_right (f2,( lim_right (f1,x0))));

        then

         A24: (f2 /* q) is convergent by A2, A22, A23, A19, LIMFUNC2:def 8;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim_right (f2,( lim_right (f1,x0)))) by A2, A22, A23, A19, LIMFUNC2:def 8;

        hence ( lim ((f2 * f1) /* s)) = ( lim_right (f2,( lim_right (f1,x0)))) by A24, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is_right_convergent_in x0 by A3, LIMFUNC2:def 4;

      hence thesis by A6, LIMFUNC2:def 8;

    end;

    theorem :: LIMFUNC4:63

    f1 is_left_convergent_in x0 & f2 is_right_convergent_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds ( lim_left (f1,x0)) < (f1 . r)) implies (f2 * f1) is_left_convergent_in x0 & ( lim_left ((f2 * f1),x0)) = ( lim_right (f2,( lim_left (f1,x0))))

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_right_convergent_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds ( lim_left (f1,x0)) < (f1 . r);

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A9: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A7, Lm1, LIMFUNC2: 1;

        

         A10: ( rng s) c= ( dom f1) by A8, Th1;

        set q = ((f1 /* s) ^\ k);

        

         A11: ( rng s) c= ( dom (f2 * f1)) by A8, Th1;

        

         A12: ( rng s) c= ( left_open_halfline x0) by A8, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A13: (q . n) = x by FUNCT_2: 113;

          

           A14: (n + k) in NAT by ORDINAL1:def 12;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A10, FUNCT_2: 108, A14

          .= x by A13, NAT_1:def 3;

          

           A16: (x0 - g) < (s . (n + k)) by A9, NAT_1: 12;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A12;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A16;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A10, A17, XBOOLE_0:def 4;

          then ( lim_left (f1,x0)) < (f1 . (s . (n + k))) by A5;

          then (f1 . (s . (n + k))) in { r1 : ( lim_left (f1,x0)) < r1 };

          then

           A18: (f1 . (s . (n + k))) in ( right_open_halfline ( lim_left (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A11, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim_left (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim_left (f1,x0))));

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th1;

        

        then

         A20: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A11, VALUED_0: 31;

        

         A21: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A8, Th1;

        then

         A22: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC2:def 7;

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A7, A21, LIMFUNC2:def 7;

        then

         A23: ( lim q) = ( lim_left (f1,x0)) by A22, SEQ_4: 20;

        ( lim_right (f2,( lim_left (f1,x0)))) = ( lim_right (f2,( lim_left (f1,x0))));

        then

         A24: (f2 /* q) is convergent by A2, A22, A23, A19, LIMFUNC2:def 8;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim_right (f2,( lim_left (f1,x0)))) by A2, A22, A23, A19, LIMFUNC2:def 8;

        hence ( lim ((f2 * f1) /* s)) = ( lim_right (f2,( lim_left (f1,x0)))) by A24, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is_left_convergent_in x0 by A3, LIMFUNC2:def 1;

      hence thesis by A6, LIMFUNC2:def 7;

    end;

    theorem :: LIMFUNC4:64

    f1 is_right_convergent_in x0 & f2 is_left_convergent_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) < ( lim_right (f1,x0))) implies (f2 * f1) is_right_convergent_in x0 & ( lim_right ((f2 * f1),x0)) = ( lim_left (f2,( lim_right (f1,x0))))

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_left_convergent_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) < ( lim_right (f1,x0));

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A9: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A7, Lm1, LIMFUNC2: 2;

        

         A10: ( rng s) c= ( dom f1) by A8, Th1;

        set q = ((f1 /* s) ^\ k);

        

         A11: ( rng s) c= ( dom (f2 * f1)) by A8, Th1;

        

         A12: ( rng s) c= ( right_open_halfline x0) by A8, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A13: (q . n) = x by FUNCT_2: 113;

          

           A14: (n + k) in NAT by ORDINAL1:def 12;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A10, FUNCT_2: 108, A14

          .= x by A13, NAT_1:def 3;

          

           A16: (s . (n + k)) < (x0 + g) by A9, NAT_1: 12;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A12;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A16;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_right (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { r1 : r1 < ( lim_right (f1,x0)) };

          then

           A18: (f1 . (s . (n + k))) in ( left_open_halfline ( lim_right (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A11, A17, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim_right (f1,x0)))) by A18, A15, XBOOLE_0:def 4;

        end;

        then

         A19: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim_right (f1,x0))));

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th1;

        

        then

         A20: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A11, VALUED_0: 31;

        

         A21: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A8, Th1;

        then

         A22: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC2:def 8;

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A7, A21, LIMFUNC2:def 8;

        then

         A23: ( lim q) = ( lim_right (f1,x0)) by A22, SEQ_4: 20;

        ( lim_left (f2,( lim_right (f1,x0)))) = ( lim_left (f2,( lim_right (f1,x0))));

        then

         A24: (f2 /* q) is convergent by A2, A22, A23, A19, LIMFUNC2:def 7;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim_left (f2,( lim_right (f1,x0)))) by A2, A22, A23, A19, LIMFUNC2:def 7;

        hence ( lim ((f2 * f1) /* s)) = ( lim_left (f2,( lim_right (f1,x0)))) by A24, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is_right_convergent_in x0 by A3, LIMFUNC2:def 4;

      hence thesis by A6, LIMFUNC2:def 8;

    end;

    theorem :: LIMFUNC4:65

    f1 is convergent_in+infty & f2 is_left_convergent_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) < ( lim_in+infty f1)) implies (f2 * f1) is convergent_in+infty & ( lim_in+infty (f2 * f1)) = ( lim_left (f2,( lim_in+infty f1)))

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_left_convergent_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) < ( lim_in+infty f1);

       A5:

      now

        set L = ( lim_left (f2,( lim_in+infty f1)));

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to+infty and

         A7: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds r < (s . n) by A6;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A6, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A7, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        then ( rng q) c= ( dom f1) by A10;

        then

         A12: (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        

         A13: ( rng (f1 /* s)) c= ( dom f2) by A7, Lm2;

        

         A14: ( rng (f1 /* q)) c= (( dom f2) /\ ( left_open_halfline ( lim_in+infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A15: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A16: x = (f1 . (q . n)) by A10, A11, A15, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A8, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A17: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_in+infty f1) by A4;

          then x in { g1 : g1 < ( lim_in+infty f1) } by A16;

          then

           A18: x in ( left_open_halfline ( lim_in+infty f1)) by XXREAL_1: 229;

          

           A19: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A13;

          then x in ( dom f2) by A10, A16, FUNCT_2: 108, A19;

          hence thesis by A18, XBOOLE_0:def 4;

        end;

        

         A20: (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A13, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A7, VALUED_0: 31;

        L = L;

        then

         A21: (f2 /* (f1 /* q)) is convergent by A2, A12, A14, LIMFUNC2:def 7;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* (f1 /* q))) = L by A2, A12, A14, LIMFUNC2:def 7;

        hence ( lim ((f2 * f1) /* s)) = L by A21, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is convergent_in+infty by A3;

      hence thesis by A5, LIMFUNC1:def 12;

    end;

    theorem :: LIMFUNC4:66

    f1 is convergent_in+infty & f2 is_right_convergent_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds ( lim_in+infty f1) < (f1 . g)) implies (f2 * f1) is convergent_in+infty & ( lim_in+infty (f2 * f1)) = ( lim_right (f2,( lim_in+infty f1)))

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_right_convergent_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds ( lim_in+infty f1) < (f1 . g);

       A5:

      now

        set L = ( lim_right (f2,( lim_in+infty f1)));

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to+infty and

         A7: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds r < (s . n) by A6;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A6, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A7, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        then ( rng q) c= ( dom f1) by A10;

        then

         A12: (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        

         A13: ( rng (f1 /* s)) c= ( dom f2) by A7, Lm2;

        

         A14: ( rng (f1 /* q)) c= (( dom f2) /\ ( right_open_halfline ( lim_in+infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A15: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A16: x = (f1 . (q . n)) by A10, A11, A15, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A8, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A17: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A17, XBOOLE_0:def 4;

          then ( lim_in+infty f1) < (f1 . (s . (n + k))) by A4;

          then x in { g1 : ( lim_in+infty f1) < g1 } by A16;

          then

           A18: x in ( right_open_halfline ( lim_in+infty f1)) by XXREAL_1: 230;

          

           A19: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A13;

          then x in ( dom f2) by A10, A16, FUNCT_2: 108, A19;

          hence thesis by A18, XBOOLE_0:def 4;

        end;

        

         A20: (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A13, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A7, VALUED_0: 31;

        L = L;

        then

         A21: (f2 /* (f1 /* q)) is convergent by A2, A12, A14, LIMFUNC2:def 8;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* (f1 /* q))) = L by A2, A12, A14, LIMFUNC2:def 8;

        hence ( lim ((f2 * f1) /* s)) = L by A21, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is convergent_in+infty by A3;

      hence thesis by A5, LIMFUNC1:def 12;

    end;

    theorem :: LIMFUNC4:67

    f1 is convergent_in-infty & f2 is_left_convergent_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) < ( lim_in-infty f1)) implies (f2 * f1) is convergent_in-infty & ( lim_in-infty (f2 * f1)) = ( lim_left (f2,( lim_in-infty f1)))

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_left_convergent_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) < ( lim_in-infty f1);

       A5:

      now

        set L = ( lim_left (f2,( lim_in-infty f1)));

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to-infty and

         A7: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < r by A6;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A6, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A7, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        then ( rng q) c= ( dom f1) by A10;

        then

         A12: (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        

         A13: ( rng (f1 /* s)) c= ( dom f2) by A7, Lm2;

        

         A14: ( rng (f1 /* q)) c= (( dom f2) /\ ( left_open_halfline ( lim_in-infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A15: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A16: x = (f1 . (q . n)) by A10, A11, A15, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A8, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A17: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim_in-infty f1) by A4;

          then x in { g1 : g1 < ( lim_in-infty f1) } by A16;

          then

           A18: x in ( left_open_halfline ( lim_in-infty f1)) by XXREAL_1: 229;

          

           A19: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A13;

          then x in ( dom f2) by A10, A16, FUNCT_2: 108, A19;

          hence thesis by A18, XBOOLE_0:def 4;

        end;

        

         A20: (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A13, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A7, VALUED_0: 31;

        L = L;

        then

         A21: (f2 /* (f1 /* q)) is convergent by A2, A12, A14, LIMFUNC2:def 7;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* (f1 /* q))) = L by A2, A12, A14, LIMFUNC2:def 7;

        hence ( lim ((f2 * f1) /* s)) = L by A21, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is convergent_in-infty by A3;

      hence thesis by A5, LIMFUNC1:def 13;

    end;

    theorem :: LIMFUNC4:68

    f1 is convergent_in-infty & f2 is_right_convergent_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds ( lim_in-infty f1) < (f1 . g)) implies (f2 * f1) is convergent_in-infty & ( lim_in-infty (f2 * f1)) = ( lim_right (f2,( lim_in-infty f1)))

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_right_convergent_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds ( lim_in-infty f1) < (f1 . g);

       A5:

      now

        set L = ( lim_right (f2,( lim_in-infty f1)));

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to-infty and

         A7: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < r by A6;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A6, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A7, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        then ( rng q) c= ( dom f1) by A10;

        then

         A12: (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        

         A13: ( rng (f1 /* s)) c= ( dom f2) by A7, Lm2;

        

         A14: ( rng (f1 /* q)) c= (( dom f2) /\ ( right_open_halfline ( lim_in-infty f1)))

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A15: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A16: x = (f1 . (q . n)) by A10, A11, A15, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A8, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A17: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A17, XBOOLE_0:def 4;

          then ( lim_in-infty f1) < (f1 . (s . (n + k))) by A4;

          then x in { g1 : ( lim_in-infty f1) < g1 } by A16;

          then

           A18: x in ( right_open_halfline ( lim_in-infty f1)) by XXREAL_1: 230;

          

           A19: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A13;

          then x in ( dom f2) by A10, A16, FUNCT_2: 108, A19;

          hence thesis by A18, XBOOLE_0:def 4;

        end;

        

         A20: (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A13, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A7, VALUED_0: 31;

        L = L;

        then

         A21: (f2 /* (f1 /* q)) is convergent by A2, A12, A14, LIMFUNC2:def 8;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* (f1 /* q))) = L by A2, A12, A14, LIMFUNC2:def 8;

        hence ( lim ((f2 * f1) /* s)) = L by A21, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is convergent_in-infty by A3;

      hence thesis by A5, LIMFUNC1:def 13;

    end;

    theorem :: LIMFUNC4:69

    f1 is_divergent_to+infty_in x0 & f2 is convergent_in+infty & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) implies (f2 * f1) is_convergent_in x0 & ( lim ((f2 * f1),x0)) = ( lim_in+infty f2)

    proof

      assume that

       A1: f1 is_divergent_to+infty_in x0 and

       A2: f2 is convergent_in+infty and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent & ( lim s) = x0 and

         A6: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        ( rng s) c= (( dom f1) \ {x0}) by A6, Th2;

        then

         A7: (f1 /* s) is divergent_to+infty by A1, A5, LIMFUNC3:def 2;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Th2;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in+infty f2) by A2, A7, LIMFUNC1:def 12;

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A6, Th2;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in+infty f2) by A10, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is_convergent_in x0 by A3, LIMFUNC3:def 1;

      hence thesis by A4, LIMFUNC3:def 4;

    end;

    theorem :: LIMFUNC4:70

    f1 is_divergent_to-infty_in x0 & f2 is convergent_in-infty & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) implies (f2 * f1) is_convergent_in x0 & ( lim ((f2 * f1),x0)) = ( lim_in-infty f2)

    proof

      assume that

       A1: f1 is_divergent_to-infty_in x0 and

       A2: f2 is convergent_in-infty and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

       A4:

      now

        let s be Real_Sequence;

        assume that

         A5: s is convergent & ( lim s) = x0 and

         A6: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        ( rng s) c= (( dom f1) \ {x0}) by A6, Th2;

        then

         A7: (f1 /* s) is divergent_to-infty by A1, A5, LIMFUNC3:def 3;

        

         A8: ( rng (f1 /* s)) c= ( dom f2) by A6, Th2;

        then

         A9: ( lim (f2 /* (f1 /* s))) = ( lim_in-infty f2) by A2, A7, LIMFUNC1:def 13;

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A6, Th2;

        (f2 /* (f1 /* s)) is convergent by A2, A8, A7;

        hence ((f2 * f1) /* s) is convergent & ( lim ((f2 * f1) /* s)) = ( lim_in-infty f2) by A10, A9, VALUED_0: 31;

      end;

      hence (f2 * f1) is_convergent_in x0 by A3, LIMFUNC3:def 1;

      hence thesis by A4, LIMFUNC3:def 4;

    end;

    theorem :: LIMFUNC4:71

    f1 is convergent_in+infty & f2 is_convergent_in ( lim_in+infty f1) & (for r holds ex g st r < g & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <> ( lim_in+infty f1)) implies (f2 * f1) is convergent_in+infty & ( lim_in+infty (f2 * f1)) = ( lim (f2,( lim_in+infty f1)))

    proof

      assume that

       A1: f1 is convergent_in+infty and

       A2: f2 is_convergent_in ( lim_in+infty f1) and

       A3: for r holds ex g st r < g & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( right_open_halfline r)) holds (f1 . g) <> ( lim_in+infty f1);

       A5:

      now

        set L = ( lim (f2,( lim_in+infty f1)));

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to+infty and

         A7: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds r < (s . n) by A6;

        set q = (s ^\ k);

        

         A9: q is divergent_to+infty by A6, LIMFUNC1: 26;

        

         A10: ( rng s) c= ( dom f1) by A7, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        then ( rng q) c= ( dom f1) by A10;

        then

         A12: (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in+infty f1) by A1, A9, LIMFUNC1:def 12;

        

         A13: ( rng (f1 /* s)) c= ( dom f2) by A7, Lm2;

        

         A14: ( rng (f1 /* q)) c= (( dom f2) \ {( lim_in+infty f1)})

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A15: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A16: x = (f1 . (q . n)) by A10, A11, A15, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          r < (s . (n + k)) by A8, NAT_1: 12;

          then (s . (n + k)) in { r2 : r < r2 };

          then

           A17: (s . (n + k)) in ( right_open_halfline r) by XXREAL_1: 230;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( right_open_halfline r)) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_in+infty f1) by A4;

          then

           A18: not (f1 . (s . (n + k))) in {( lim_in+infty f1)} by TARSKI:def 1;

          

           A19: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A13;

          then x in ( dom f2) by A10, A16, FUNCT_2: 108, A19;

          hence thesis by A16, A18, XBOOLE_0:def 5;

        end;

        

         A20: (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A13, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A7, VALUED_0: 31;

        L = L;

        then

         A21: (f2 /* (f1 /* q)) is convergent by A2, A12, A14, LIMFUNC3:def 4;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* (f1 /* q))) = L by A2, A12, A14, LIMFUNC3:def 4;

        hence ( lim ((f2 * f1) /* s)) = L by A21, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is convergent_in+infty by A3;

      hence thesis by A5, LIMFUNC1:def 12;

    end;

    theorem :: LIMFUNC4:72

    f1 is convergent_in-infty & f2 is_convergent_in ( lim_in-infty f1) & (for r holds ex g st g < r & g in ( dom (f2 * f1))) & (ex r st for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <> ( lim_in-infty f1)) implies (f2 * f1) is convergent_in-infty & ( lim_in-infty (f2 * f1)) = ( lim (f2,( lim_in-infty f1)))

    proof

      assume that

       A1: f1 is convergent_in-infty and

       A2: f2 is_convergent_in ( lim_in-infty f1) and

       A3: for r holds ex g st g < r & g in ( dom (f2 * f1));

      given r such that

       A4: for g st g in (( dom f1) /\ ( left_open_halfline r)) holds (f1 . g) <> ( lim_in-infty f1);

       A5:

      now

        set L = ( lim (f2,( lim_in-infty f1)));

        let s be Real_Sequence;

        assume that

         A6: s is divergent_to-infty and

         A7: ( rng s) c= ( dom (f2 * f1));

        consider k be Nat such that

         A8: for n be Nat st k <= n holds (s . n) < r by A6;

        set q = (s ^\ k);

        

         A9: q is divergent_to-infty by A6, LIMFUNC1: 27;

        

         A10: ( rng s) c= ( dom f1) by A7, Lm2;

        

         A11: ( rng q) c= ( rng s) by VALUED_0: 21;

        then ( rng q) c= ( dom f1) by A10;

        then

         A12: (f1 /* q) is convergent & ( lim (f1 /* q)) = ( lim_in-infty f1) by A1, A9, LIMFUNC1:def 13;

        

         A13: ( rng (f1 /* s)) c= ( dom f2) by A7, Lm2;

        

         A14: ( rng (f1 /* q)) c= (( dom f2) \ {( lim_in-infty f1)})

        proof

          let x be object;

          assume x in ( rng (f1 /* q));

          then

          consider n be Element of NAT such that

           A15: ((f1 /* q) . n) = x by FUNCT_2: 113;

          

           A16: x = (f1 . (q . n)) by A10, A11, A15, FUNCT_2: 108, XBOOLE_1: 1

          .= (f1 . (s . (n + k))) by NAT_1:def 3;

          (s . (n + k)) < r by A8, NAT_1: 12;

          then (s . (n + k)) in { r2 : r2 < r };

          then

           A17: (s . (n + k)) in ( left_open_halfline r) by XXREAL_1: 229;

          (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in (( dom f1) /\ ( left_open_halfline r)) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_in-infty f1) by A4;

          then

           A18: not (f1 . (s . (n + k))) in {( lim_in-infty f1)} by TARSKI:def 1;

          

           A19: (n + k) in NAT by ORDINAL1:def 12;

          ((f1 /* s) . (n + k)) in ( rng (f1 /* s)) by VALUED_0: 28;

          then ((f1 /* s) . (n + k)) in ( dom f2) by A13;

          then x in ( dom f2) by A10, A16, FUNCT_2: 108, A19;

          hence thesis by A16, A18, XBOOLE_0:def 5;

        end;

        

         A20: (f2 /* (f1 /* q)) = (f2 /* ((f1 /* s) ^\ k)) by A10, VALUED_0: 27

        .= ((f2 /* (f1 /* s)) ^\ k) by A13, VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A7, VALUED_0: 31;

        L = L;

        then

         A21: (f2 /* (f1 /* q)) is convergent by A2, A12, A14, LIMFUNC3:def 4;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* (f1 /* q))) = L by A2, A12, A14, LIMFUNC3:def 4;

        hence ( lim ((f2 * f1) /* s)) = L by A21, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is convergent_in-infty by A3;

      hence thesis by A5, LIMFUNC1:def 13;

    end;

    theorem :: LIMFUNC4:73

    f1 is_convergent_in x0 & f2 is_left_convergent_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) < ( lim (f1,x0))) implies (f2 * f1) is_convergent_in x0 & ( lim ((f2 * f1),x0)) = ( lim_left (f2,( lim (f1,x0))))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_left_convergent_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) < ( lim (f1,x0));

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A9: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A7, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A8, Th2;

        

         A11: ( rng s) c= ( dom f1) by A8, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A12: (q . n) = x by FUNCT_2: 113;

          

           A13: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A11, FUNCT_2: 108

          .= x by A12, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A9;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A14: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A15: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A8, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A14, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A11, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) < ( lim (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { g2 : g2 < ( lim (f1,x0)) };

          then

           A16: (f1 . (s . (n + k))) in ( left_open_halfline ( lim (f1,x0))) by XXREAL_1: 229;

          (f1 . (s . (n + k))) in ( dom f2) by A10, A15, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( left_open_halfline ( lim (f1,x0)))) by A16, A13, XBOOLE_0:def 4;

        end;

        then

         A17: ( rng q) c= (( dom f2) /\ ( left_open_halfline ( lim (f1,x0))));

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th2;

        

        then

         A18: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A10, VALUED_0: 31;

        

         A19: ( rng s) c= (( dom f1) \ {x0}) by A8, Th2;

        then

         A20: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC3:def 4;

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A7, A19, LIMFUNC3:def 4;

        then

         A21: ( lim q) = ( lim (f1,x0)) by A20, SEQ_4: 20;

        ( lim_left (f2,( lim (f1,x0)))) = ( lim_left (f2,( lim (f1,x0))));

        then

         A22: (f2 /* q) is convergent by A2, A20, A21, A17, LIMFUNC2:def 7;

        hence ((f2 * f1) /* s) is convergent by A18, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim_left (f2,( lim (f1,x0)))) by A2, A20, A21, A17, LIMFUNC2:def 7;

        hence ( lim ((f2 * f1) /* s)) = ( lim_left (f2,( lim (f1,x0)))) by A22, A18, SEQ_4: 22;

      end;

      hence (f2 * f1) is_convergent_in x0 by A3, LIMFUNC3:def 1;

      hence thesis by A6, LIMFUNC3:def 4;

    end;

    theorem :: LIMFUNC4:74

    f1 is_left_convergent_in x0 & f2 is_convergent_in ( lim_left (f1,x0)) & (for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) <> ( lim_left (f1,x0))) implies (f2 * f1) is_left_convergent_in x0 & ( lim_left ((f2 * f1),x0)) = ( lim (f2,( lim_left (f1,x0))))

    proof

      assume that

       A1: f1 is_left_convergent_in x0 and

       A2: f2 is_convergent_in ( lim_left (f1,x0)) and

       A3: for r st r < x0 holds ex g st r < g & g < x0 & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].(x0 - g), x0.[) holds (f1 . r) <> ( lim_left (f1,x0));

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) /\ ( left_open_halfline x0));

        consider k be Nat such that

         A9: for n be Nat st k <= n holds (x0 - g) < (s . n) by A4, A7, Lm1, LIMFUNC2: 1;

        

         A10: ( rng s) c= ( dom f1) by A8, Th1;

        set q = ((f1 /* s) ^\ k);

        

         A11: ( rng s) c= ( dom (f2 * f1)) by A8, Th1;

        

         A12: ( rng s) c= ( left_open_halfline x0) by A8, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A13: (q . n) = x by FUNCT_2: 113;

          

           A14: (n + k) in NAT by ORDINAL1:def 12;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A10, FUNCT_2: 108, A14

          .= x by A13, NAT_1:def 3;

          

           A16: (x0 - g) < (s . (n + k)) by A9, NAT_1: 12;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( left_open_halfline x0) by A12;

          then (s . (n + k)) in { g1 : g1 < x0 } by XXREAL_1: 229;

          then ex g1 st g1 = (s . (n + k)) & g1 < x0;

          then (s . (n + k)) in { g2 : (x0 - g) < g2 & g2 < x0 } by A16;

          then (s . (n + k)) in ].(x0 - g), x0.[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].(x0 - g), x0.[) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_left (f1,x0)) by A5;

          then

           A18: not (f1 . (s . (n + k))) in {( lim_left (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A11, A17, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim_left (f1,x0))}) by A18, A15, XBOOLE_0:def 5;

        end;

        then

         A19: ( rng q) c= (( dom f2) \ {( lim_left (f1,x0))});

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th1;

        

        then

         A20: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A11, VALUED_0: 31;

        

         A21: ( rng s) c= (( dom f1) /\ ( left_open_halfline x0)) by A8, Th1;

        then

         A22: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC2:def 7;

        ( lim (f1 /* s)) = ( lim_left (f1,x0)) by A1, A7, A21, LIMFUNC2:def 7;

        then

         A23: ( lim q) = ( lim_left (f1,x0)) by A22, SEQ_4: 20;

        ( lim (f2,( lim_left (f1,x0)))) = ( lim (f2,( lim_left (f1,x0))));

        then

         A24: (f2 /* q) is convergent by A2, A22, A23, A19, LIMFUNC3:def 4;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim (f2,( lim_left (f1,x0)))) by A2, A22, A23, A19, LIMFUNC3:def 4;

        hence ( lim ((f2 * f1) /* s)) = ( lim (f2,( lim_left (f1,x0)))) by A24, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is_left_convergent_in x0 by A3, LIMFUNC2:def 1;

      hence thesis by A6, LIMFUNC2:def 7;

    end;

    theorem :: LIMFUNC4:75

    f1 is_convergent_in x0 & f2 is_right_convergent_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds ( lim (f1,x0)) < (f1 . r)) implies (f2 * f1) is_convergent_in x0 & ( lim ((f2 * f1),x0)) = ( lim_right (f2,( lim (f1,x0))))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_right_convergent_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds ( lim (f1,x0)) < (f1 . r);

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A9: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A7, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A8, Th2;

        

         A11: ( rng s) c= ( dom f1) by A8, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A12: (q . n) = x by FUNCT_2: 113;

          

           A13: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A11, FUNCT_2: 108

          .= x by A12, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A9;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A14: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A15: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A8, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A14, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A11, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) > ( lim (f1,x0)) by A5;

          then (f1 . (s . (n + k))) in { g2 : ( lim (f1,x0)) < g2 };

          then

           A16: (f1 . (s . (n + k))) in ( right_open_halfline ( lim (f1,x0))) by XXREAL_1: 230;

          (f1 . (s . (n + k))) in ( dom f2) by A10, A15, FUNCT_1: 11;

          hence x in (( dom f2) /\ ( right_open_halfline ( lim (f1,x0)))) by A16, A13, XBOOLE_0:def 4;

        end;

        then

         A17: ( rng q) c= (( dom f2) /\ ( right_open_halfline ( lim (f1,x0))));

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th2;

        

        then

         A18: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A10, VALUED_0: 31;

        

         A19: ( rng s) c= (( dom f1) \ {x0}) by A8, Th2;

        then

         A20: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC3:def 4;

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A7, A19, LIMFUNC3:def 4;

        then

         A21: ( lim q) = ( lim (f1,x0)) by A20, SEQ_4: 20;

        ( lim_right (f2,( lim (f1,x0)))) = ( lim_right (f2,( lim (f1,x0))));

        then

         A22: (f2 /* q) is convergent by A2, A20, A21, A17, LIMFUNC2:def 8;

        hence ((f2 * f1) /* s) is convergent by A18, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim_right (f2,( lim (f1,x0)))) by A2, A20, A21, A17, LIMFUNC2:def 8;

        hence ( lim ((f2 * f1) /* s)) = ( lim_right (f2,( lim (f1,x0)))) by A22, A18, SEQ_4: 22;

      end;

      hence (f2 * f1) is_convergent_in x0 by A3, LIMFUNC3:def 1;

      hence thesis by A6, LIMFUNC3:def 4;

    end;

    theorem :: LIMFUNC4:76

    f1 is_right_convergent_in x0 & f2 is_convergent_in ( lim_right (f1,x0)) & (for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) <> ( lim_right (f1,x0))) implies (f2 * f1) is_right_convergent_in x0 & ( lim_right ((f2 * f1),x0)) = ( lim (f2,( lim_right (f1,x0))))

    proof

      assume that

       A1: f1 is_right_convergent_in x0 and

       A2: f2 is_convergent_in ( lim_right (f1,x0)) and

       A3: for r st x0 < r holds ex g st g < r & x0 < g & g in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ].x0, (x0 + g).[) holds (f1 . r) <> ( lim_right (f1,x0));

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) /\ ( right_open_halfline x0));

        consider k be Nat such that

         A9: for n be Nat st k <= n holds (s . n) < (x0 + g) by A4, A7, Lm1, LIMFUNC2: 2;

        

         A10: ( rng s) c= ( dom f1) by A8, Th1;

        set q = ((f1 /* s) ^\ k);

        

         A11: ( rng s) c= ( dom (f2 * f1)) by A8, Th1;

        

         A12: ( rng s) c= ( right_open_halfline x0) by A8, Th1;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A13: (q . n) = x by FUNCT_2: 113;

          

           A14: (n + k) in NAT by ORDINAL1:def 12;

          

           A15: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A10, FUNCT_2: 108, A14

          .= x by A13, NAT_1:def 3;

          

           A16: (s . (n + k)) < (x0 + g) by A9, NAT_1: 12;

          

           A17: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then (s . (n + k)) in ( right_open_halfline x0) by A12;

          then (s . (n + k)) in { g1 : x0 < g1 } by XXREAL_1: 230;

          then ex g1 st g1 = (s . (n + k)) & x0 < g1;

          then (s . (n + k)) in { g2 : x0 < g2 & g2 < (x0 + g) } by A16;

          then (s . (n + k)) in ].x0, (x0 + g).[ by RCOMP_1:def 2;

          then (s . (n + k)) in (( dom f1) /\ ].x0, (x0 + g).[) by A10, A17, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim_right (f1,x0)) by A5;

          then

           A18: not (f1 . (s . (n + k))) in {( lim_right (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A11, A17, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim_right (f1,x0))}) by A18, A15, XBOOLE_0:def 5;

        end;

        then

         A19: ( rng q) c= (( dom f2) \ {( lim_right (f1,x0))});

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th1;

        

        then

         A20: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A11, VALUED_0: 31;

        

         A21: ( rng s) c= (( dom f1) /\ ( right_open_halfline x0)) by A8, Th1;

        then

         A22: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC2:def 8;

        ( lim (f1 /* s)) = ( lim_right (f1,x0)) by A1, A7, A21, LIMFUNC2:def 8;

        then

         A23: ( lim q) = ( lim_right (f1,x0)) by A22, SEQ_4: 20;

        ( lim (f2,( lim_right (f1,x0)))) = ( lim (f2,( lim_right (f1,x0))));

        then

         A24: (f2 /* q) is convergent by A2, A22, A23, A19, LIMFUNC3:def 4;

        hence ((f2 * f1) /* s) is convergent by A20, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim (f2,( lim_right (f1,x0)))) by A2, A22, A23, A19, LIMFUNC3:def 4;

        hence ( lim ((f2 * f1) /* s)) = ( lim (f2,( lim_right (f1,x0)))) by A24, A20, SEQ_4: 22;

      end;

      hence (f2 * f1) is_right_convergent_in x0 by A3, LIMFUNC2:def 4;

      hence thesis by A6, LIMFUNC2:def 8;

    end;

    theorem :: LIMFUNC4:77

    f1 is_convergent_in x0 & f2 is_convergent_in ( lim (f1,x0)) & (for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1))) & (ex g st 0 < g & for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) <> ( lim (f1,x0))) implies (f2 * f1) is_convergent_in x0 & ( lim ((f2 * f1),x0)) = ( lim (f2,( lim (f1,x0))))

    proof

      assume that

       A1: f1 is_convergent_in x0 and

       A2: f2 is_convergent_in ( lim (f1,x0)) and

       A3: for r1, r2 st r1 < x0 & x0 < r2 holds ex g1, g2 st r1 < g1 & g1 < x0 & g1 in ( dom (f2 * f1)) & g2 < r2 & x0 < g2 & g2 in ( dom (f2 * f1));

      given g such that

       A4: 0 < g and

       A5: for r st r in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) holds (f1 . r) <> ( lim (f1,x0));

       A6:

      now

        let s be Real_Sequence;

        assume that

         A7: s is convergent & ( lim s) = x0 and

         A8: ( rng s) c= (( dom (f2 * f1)) \ {x0});

        consider k be Element of NAT such that

         A9: for n be Element of NAT st k <= n holds (x0 - g) < (s . n) & (s . n) < (x0 + g) by A4, A7, LIMFUNC3: 7;

        set q = ((f1 /* s) ^\ k);

        

         A10: ( rng s) c= ( dom (f2 * f1)) by A8, Th2;

        

         A11: ( rng s) c= ( dom f1) by A8, Th2;

        now

          let x be object;

          assume x in ( rng q);

          then

          consider n be Element of NAT such that

           A12: (q . n) = x by FUNCT_2: 113;

          

           A13: (f1 . (s . (n + k))) = ((f1 /* s) . (n + k)) by A11, FUNCT_2: 108

          .= x by A12, NAT_1:def 3;

          k <= (n + k) by NAT_1: 12;

          then (x0 - g) < (s . (n + k)) & (s . (n + k)) < (x0 + g) by A9;

          then (s . (n + k)) in { g1 : (x0 - g) < g1 & g1 < (x0 + g) };

          then

           A14: (s . (n + k)) in ].(x0 - g), (x0 + g).[ by RCOMP_1:def 2;

          

           A15: (s . (n + k)) in ( rng s) by VALUED_0: 28;

          then not (s . (n + k)) in {x0} by A8, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), (x0 + g).[ \ {x0}) by A14, XBOOLE_0:def 5;

          then (s . (n + k)) in ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[) by A4, LIMFUNC3: 4;

          then (s . (n + k)) in (( dom f1) /\ ( ].(x0 - g), x0.[ \/ ].x0, (x0 + g).[)) by A11, A15, XBOOLE_0:def 4;

          then (f1 . (s . (n + k))) <> ( lim (f1,x0)) by A5;

          then

           A16: not (f1 . (s . (n + k))) in {( lim (f1,x0))} by TARSKI:def 1;

          (f1 . (s . (n + k))) in ( dom f2) by A10, A15, FUNCT_1: 11;

          hence x in (( dom f2) \ {( lim (f1,x0))}) by A16, A13, XBOOLE_0:def 5;

        end;

        then

         A17: ( rng q) c= (( dom f2) \ {( lim (f1,x0))});

        ( rng (f1 /* s)) c= ( dom f2) by A8, Th2;

        

        then

         A18: (f2 /* q) = ((f2 /* (f1 /* s)) ^\ k) by VALUED_0: 27

        .= (((f2 * f1) /* s) ^\ k) by A10, VALUED_0: 31;

        

         A19: ( rng s) c= (( dom f1) \ {x0}) by A8, Th2;

        then

         A20: (f1 /* s) is convergent by A1, A2, A7, LIMFUNC3:def 4;

        ( lim (f1 /* s)) = ( lim (f1,x0)) by A1, A7, A19, LIMFUNC3:def 4;

        then

         A21: ( lim q) = ( lim (f1,x0)) by A20, SEQ_4: 20;

        ( lim (f2,( lim (f1,x0)))) = ( lim (f2,( lim (f1,x0))));

        then

         A22: (f2 /* q) is convergent by A2, A20, A21, A17, LIMFUNC3:def 4;

        hence ((f2 * f1) /* s) is convergent by A18, SEQ_4: 21;

        ( lim (f2 /* q)) = ( lim (f2,( lim (f1,x0)))) by A2, A20, A21, A17, LIMFUNC3:def 4;

        hence ( lim ((f2 * f1) /* s)) = ( lim (f2,( lim (f1,x0)))) by A22, A18, SEQ_4: 22;

      end;

      hence (f2 * f1) is_convergent_in x0 by A3, LIMFUNC3:def 1;

      hence thesis by A6, LIMFUNC3:def 4;

    end;