ordeq_02.miz



    begin

    reserve Y for RealNormSpace;

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

    

     Lm1: the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

    

     Lm2: ( dom ( proj (1,1))) = ( REAL 1) & ( rng ( proj (1,1))) = REAL & for x be Element of REAL holds (( proj (1,1)) . <*x*>) = x & ((( proj (1,1)) qua Function " ) . x) = <*x*>

    proof

      set f = ( proj (1,1));

      for y be object st y in REAL holds ex x be object st x in ( REAL 1) & y = (f . x)

      proof

        let y be object;

        assume y in REAL ;

        then

        reconsider y1 = y as Element of REAL ;

        reconsider x = <*y1*> as Element of ( REAL 1) by FINSEQ_2: 98;

        (f . x) = (x . 1) by PDIFF_1:def 1;

        then (f . x) = y by FINSEQ_1: 40;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 10, FUNCT_2:def 1, PDIFF_1: 1;

    end;

    theorem :: ORDEQ_02:1

    

     NDIFF435: for Y be RealNormSpace, J be Function of ( REAL-NS 1), REAL , x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y st J = ( proj (1,1)) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & f = (g * J) holds f is_continuous_in x0 iff g is_continuous_in y0

    proof

      let Y be RealNormSpace, J be Function of ( REAL-NS 1), REAL , x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y;

      assume

       A1: J = ( proj (1,1)) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & f = (g * J);

      thus f is_continuous_in x0 implies g is_continuous_in y0

      proof

        reconsider I = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL-NS 1) by PDIFF_1: 2, REAL_NS1:def 4;

        

         A2: (J * I) = ( id REAL ) by A1, Lm2, FUNCT_1: 39;

        (f * I) = (g * ( id REAL )) by A1, A2, RELAT_1: 36;

        then

         A3: (f * I) = g by FUNCT_2: 17;

        (I /. y0) = x0 by A1, PDIFF_1: 1;

        hence thesis by A3, NDIFF_4: 33, A1, NFCONT_3: 15;

      end;

      (J /. x0) = y0 by A1, PDIFF_1: 1;

      hence thesis by A1, NDIFF_4: 32, NDIFF_4: 34;

    end;

    theorem :: ORDEQ_02:2

    for Y be RealNormSpace, I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y st I = (( proj (1,1)) qua Function " ) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & (f * I) = g holds f is_continuous_in x0 iff g is_continuous_in y0

    proof

      let Y be RealNormSpace, I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y;

      assume

       A1: I = (( proj (1,1)) qua Function " ) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & (f * I) = g;

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

      thus f is_continuous_in x0 implies g is_continuous_in y0

      proof

        (I /. y0) = x0 by A1, PDIFF_1: 1;

        hence thesis by A1, NDIFF_4: 33, NFCONT_3: 15;

      end;

      

       A2: (I * J) = ( id ( REAL-NS 1)) by A1, Lm2, Lm1, FUNCT_1: 39;

      

       A3: (g * J) = (f * ( id ( REAL-NS 1))) by A2, A1, RELAT_1: 36

      .= f by FUNCT_2: 17;

      (J /. x0) = y0 by A1, PDIFF_1: 1;

      hence thesis by A3, NDIFF_4: 32, A1, NDIFF_4: 34;

    end;

    theorem :: ORDEQ_02:3

    

     FTh40: for I be Function of REAL , ( REAL-NS 1) st I = (( proj (1,1)) qua Function " ) holds (for R be RestFunc of ( REAL-NS 1), Y holds (R * I) is RestFunc of Y) & for L be LinearOperator of ( REAL-NS 1), Y holds (L * I) is LinearFunc of Y

    proof

      let I be Function of REAL , ( REAL-NS 1);

      assume

       A1: I = (( proj (1,1)) qua Function " );

      

       A0: ( dom I) = REAL by FUNCT_2:def 1;

      thus for R be RestFunc of ( REAL-NS 1), Y holds (R * I) is RestFunc of Y

      proof

        let R be RestFunc of ( REAL-NS 1), Y;

        

         A2: R is total by NDIFF_1:def 5;

        then

        reconsider R0 = R as Function of ( REAL 1), Y by Lm1;

        reconsider R1 = (R * I) as PartFunc of REAL , Y;

        

         A3: (R0 * I) is Function of REAL , Y by Lm1;

        then

         A4: ( dom R1) = REAL by FUNCT_2:def 1;

        

         A5: for r be Real st r > 0 holds ex d be Real st d > 0 & for z1 be Real st z1 <> 0 & |.z1.| < d holds (( |.z1.| " ) * ||.(R1 /. z1).||) < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider d be Real such that

           A6: d > 0 and

           A7: for z be Point of ( REAL-NS 1) st z <> ( 0. ( REAL-NS 1)) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r by A2, NDIFF_1: 23;

          take d;

          for z1 be Real st z1 <> 0 & |.z1.| < d holds (( |.z1.| " ) * ||.(R1 /. z1).||) < r

          proof

            let z1 be Real such that

             A8: z1 <> 0 and

             A9: |.z1.| < d;

            reconsider zz = z1 as Element of REAL by XREAL_0:def 1;

            reconsider z = (I . zz) as Point of ( REAL-NS 1);

             |.zz.| > 0 by A8, COMPLEX1: 47;

            then ||.z.|| <> 0 by A1, Lm1, PDIFF_1: 3;

            then

             A10: z <> ( 0. ( REAL-NS 1));

            R is total by NDIFF_1:def 5;

            then ( dom R) = the carrier of ( REAL-NS 1) by PARTFUN1:def 2;

            then (R /. z) = (R . (I . z1)) by PARTFUN1:def 6;

            then (R /. z) = (R1 . zz) by A0, FUNCT_1: 13;

            then

             A12: ||.(R /. z).|| = ||.(R1 /. zz).|| by A4, PARTFUN1:def 6;

            

             A13: ( ||.z.|| " ) = ( |.z1.| " ) by A1, Lm1, PDIFF_1: 3;

             ||.z.|| < d by A1, A9, Lm1, PDIFF_1: 3;

            hence thesis by A7, A10, A13, A12;

          end;

          hence thesis by A6;

        end;

        for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = ( 0. Y)

        proof

          let h be 0 -convergent non-zero Real_Sequence;

           A14:

          now

            let r be Real;

            

             A15: ( lim h) = 0 ;

            assume r > 0 ;

            then

            consider d be Real such that

             A16: d > 0 and

             A17: for z1 be Real st z1 <> 0 & |.z1.| < d holds (( |.z1.| " ) * ||.(R1 /. z1).||) < r by A5;

            reconsider d1 = d as Real;

            consider n0 be Nat such that

             A18: for m be Nat st n0 <= m holds |.((h . m) - 0 ).| < d1 by A16, A15, SEQ_2:def 7;

            take n0;

            hereby

              let m be Nat;

              

               A19: m in NAT by ORDINAL1:def 12;

              ( rng h) c= ( dom R1) by A4;

              

              then

               A21: (( |.(h . m).| " ) * ||.(R1 /. (h . m)).||) = (( |.(h . m).| " ) * ||.((R1 /* h) . m).||) by A19, FUNCT_2: 109

              .= (((( abs h) . m) " ) * ||.((R1 /* h) . m).||) by SEQ_1: 12

              .= (((( abs h) " ) . m) * ||.((R1 /* h) . m).||) by VALUED_1: 10

              .= (( |.(h " ).| . m) * ||.((R1 /* h) . m).||) by SEQ_1: 54

              .= ( |.((h " ) . m).| * ||.((R1 /* h) . m).||) by SEQ_1: 12

              .= ||.(((h " ) . m) * ((R1 /* h) . m)).|| by NORMSP_1:def 1

              .= ||.((((h " ) (#) (R1 /* h)) . m) - ( 0. Y)).|| by NDIFF_1:def 2;

              assume n0 <= m;

              then |.((h . m) - 0 ).| < d by A18;

              hence ||.((((h " ) (#) (R1 /* h)) . m) - ( 0. Y)).|| < r by A17, SEQ_1: 5, A21;

            end;

          end;

          hence ((h " ) (#) (R1 /* h)) is convergent;

          hence thesis by A14, NORMSP_1:def 7;

        end;

        hence thesis by A3, NDIFF_3:def 1;

      end;

      let L be LinearOperator of ( REAL-NS 1), Y;

      reconsider L0 = L as Function of ( REAL 1), Y by Lm1;

      reconsider L1 = (L0 * I) as PartFunc of REAL , Y;

      reconsider r = (L1 . jj) as Point of Y by FUNCT_2: 5;

      

       A22: ( dom (L0 * I)) = REAL & ( dom L1) = REAL by FUNCT_2:def 1;

      for p be Real holds (L1 /. p) = (p * r)

      proof

        reconsider 1p = (I . jj) as VECTOR of ( REAL-NS 1);

        let p be Real;

        (L1 . p) = (L0 . (I . (p * 1))) by A0, XREAL_0:def 1, FUNCT_1: 13;

        then (L1 . p) = (L . (p * 1p)) by A1, Lm1, PDIFF_1: 3;

        then (L1 . p) = (p * (L /. 1p)) by LOPBAN_1:def 5;

        then (L1 /. p) = (p * (L /. 1p)) by XREAL_0:def 1, A22, PARTFUN1:def 6;

        hence thesis by A22, FUNCT_1: 12;

      end;

      hence thesis by NDIFF_3:def 2;

    end;

    theorem :: ORDEQ_02:4

    

     FTh41: for J be Function of ( REAL-NS 1), REAL st J = ( proj (1,1)) holds (for R be RestFunc of Y holds (R * J) is RestFunc of ( REAL-NS 1), Y) & for L be LinearFunc of Y holds (L * J) is Lipschitzian LinearOperator of ( REAL-NS 1), Y

    proof

      let J be Function of ( REAL-NS 1), REAL ;

      assume

       A1: J = ( proj (1,1));

      thus for R be RestFunc of Y holds (R * J) is RestFunc of ( REAL-NS 1), Y

      proof

        let R be RestFunc of Y;

        

         A2: R is total by NDIFF_3:def 1;

        reconsider R0 = R as Function of REAL , Y by A2;

        reconsider R1 = (R0 * J) as PartFunc of ( REAL-NS 1), Y;

        for h be ( 0. ( REAL-NS 1)) -convergent sequence of ( REAL-NS 1) st h is non-zero holds (( ||.h.|| " ) (#) (R1 /* h)) is convergent & ( lim (( ||.h.|| " ) (#) (R1 /* h))) = ( 0. Y)

        proof

          let h be ( 0. ( REAL-NS 1)) -convergent sequence of ( REAL-NS 1);

          assume

           A3: h is non-zero;

          

           A4: ( lim h) = ( 0. ( REAL-NS 1)) by NDIFF_1:def 4;

          deffunc F( Nat) = (J . (h . $1));

          consider s be Real_Sequence such that

           A5: for n be Nat holds (s . n) = F(n) from SEQ_1:sch 1;

          

           A6: h is convergent by NDIFF_1:def 4;

           A7:

          now

            let p be Real;

            assume 0 < p;

            then

            consider m be Nat such that

             A8: for n be Nat st m <= n holds ||.((h . n) - ( 0. ( REAL-NS 1))).|| < p by A6, A4, NORMSP_1:def 7;

            take m;

            now

              let n be Nat;

              assume m <= n;

              then

               A91: ||.((h . n) - ( 0. ( REAL-NS 1))).|| < p by A8;

              (s . n) = (J . (h . n)) by A5;

              hence |.((s . n) - 0 ).| < p by A1, A91, PDIFF_1: 4;

            end;

            hence for n be Nat st m <= n holds |.((s . n) - 0 ).| < p;

          end;

          then s is convergent by SEQ_2:def 6;

          then

           A11: ( lim s) = 0 by A7, SEQ_2:def 7;

          now

            let x be object;

            assume x in NAT ;

            then

            reconsider n = x as Element of NAT ;

            

             A13: ||.(h . n).|| <> 0 by NORMSP_0:def 5, A3, NDIFF_1: 6;

            (s . n) = (J . (h . n)) by A5;

            then |.(s . n).| <> 0 by A1, A13, PDIFF_1: 4;

            hence (s . x) <> 0 by COMPLEX1: 47;

          end;

          then

          reconsider s as 0 -convergent non-zero Real_Sequence by A7, SEQ_2:def 6, A11, FDIFF_1:def 1, SEQ_1: 4;

          now

            reconsider f1 = R1 as Function;

            let n be Element of NAT ;

            ( rng h) c= the carrier of ( REAL-NS 1);

            then

             A14: ( rng h) c= ( dom R1) by FUNCT_2:def 1;

            ((R /* s) . n) = (R . (s . n)) by NDIFF_3:def 1, FUNCT_2: 115;

            then

             A15: ((R /* s) . n) = (R . (J . (h . n))) by A5;

             NAT = ( dom h) by FUNCT_2:def 1;

            then (R1 . (h . n)) = ((f1 * h) . n) by FUNCT_1: 13;

            then

             A17: (R1 . (h . n)) = ((R1 /* h) . n) by A14, FUNCT_2:def 11;

            

             A18: (s . n) = (J . (h . n)) by A5;

            ( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . n) = ||.((( ||.h.|| " ) (#) (R1 /* h)) . n).|| by NORMSP_0:def 4

            .= ||.((( ||.h.|| " ) . n) * ((R1 /* h) . n)).|| by NDIFF_1:def 2

            .= ( |.(( ||.h.|| " ) . n).| * ||.((R1 /* h) . n).||) by NORMSP_1:def 1

            .= ( |.(( ||.h.|| . n) " ).| * ||.((R1 /* h) . n).||) by VALUED_1: 10

            .= ( |.( ||.(h . n).|| " ).| * ||.((R1 /* h) . n).||) by NORMSP_0:def 4

            .= (( ||.(h . n).|| " ) * ||.((R1 /* h) . n).||) by ABSVALUE:def 1

            .= (( |.(s . n).| " ) * ||.((R1 /* h) . n).||) by A1, A18, PDIFF_1: 4

            .= (( |.(s . n).| " ) * ||.((R /* s) . n).||) by A17, A15, FUNCT_2: 15

            .= (((( abs s) . n) " ) * ||.((R /* s) . n).||) by SEQ_1: 12

            .= (((( abs s) " ) . n) * ||.((R /* s) . n).||) by VALUED_1: 10

            .= (( |.(s " ).| . n) * ||.((R /* s) . n).||) by SEQ_1: 54

            .= ( |.((s " ) . n).| * ||.((R /* s) . n).||) by SEQ_1: 12

            .= ||.(((s " ) . n) * ((R /* s) . n)).|| by NORMSP_1:def 1

            .= ||.(((s " ) (#) (R /* s)) . n).|| by NDIFF_1:def 2

            .= ( ||.((s " ) (#) (R /* s)).|| . n) by NORMSP_0:def 4;

            hence ( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . n) = ( ||.((s " ) (#) (R /* s)).|| . n);

          end;

          then

           A19: ||.(( ||.h.|| " ) (#) (R1 /* h)).|| = ||.((s " ) (#) (R /* s)).|| by FUNCT_2: 63;

          ((s " ) (#) (R /* s)) is convergent & ( lim ((s " ) (#) (R /* s))) = ( 0. Y) by NDIFF_3:def 1;

          then

           A22: ( lim ||.((s " ) (#) (R /* s)).||) = ||.( 0. Y).|| by LOPBAN_1: 20;

          

           A23: ||.((s " ) (#) (R /* s)).|| is convergent by NDIFF_3:def 1, NORMSP_1: 23;

           A24:

          now

            let p be Real;

            assume 0 < p;

            then

            consider n0 be Nat such that

             A25: for m be Nat st n0 <= m holds |.(( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . m) - 0 ).| < p by A19, A23, A22, SEQ_2:def 7;

            take n0;

            hereby

              let m be Nat;

              assume n0 <= m;

              then |.(( ||.(( ||.h.|| " ) (#) (R1 /* h)).|| . m) - 0 ).| < p by A25;

              then |. ||.((( ||.h.|| " ) (#) (R1 /* h)) . m).||.| < p by NORMSP_0:def 4;

              hence ||.(((( ||.h.|| " ) (#) (R1 /* h)) . m) - ( 0. Y)).|| < p by ABSVALUE:def 1;

            end;

          end;

          then (( ||.h.|| " ) (#) (R1 /* h)) is convergent;

          hence thesis by A24, NORMSP_1:def 7;

        end;

        hence thesis by NDIFF_1:def 5;

      end;

      let L be LinearFunc of Y;

      consider r be Point of Y such that

       A27: for p be Real holds (L /. p) = (p * r) by NDIFF_3:def 2;

      reconsider L0 = L as Function of REAL , Y;

      set K = ||.r.||;

      reconsider L1 = (L * J) as Function of ( REAL-NS 1), Y;

      

       A28: ( dom L1) = ( REAL 1) by Lm1, FUNCT_2:def 1;

       A29:

      now

        let x,y be Point of ( REAL-NS 1);

        (L1 . (x + y)) = (L /. (J . (x + y))) by Lm1, A28, FUNCT_1: 12;

        then (L1 . (x + y)) = (L /. ((J . x) + (J . y))) by A1, PDIFF_1: 4;

        then (L1 . (x + y)) = (((J . x) + (J . y)) * r) by A27;

        then (L1 . (x + y)) = (((J . x) * r) + ((J . y) * r)) by RLVECT_1:def 6;

        then (L1 . (x + y)) = ((L /. (J . x)) + ((J . y) * r)) by A27;

        then

         A30: (L1 . (x + y)) = ((L /. (J . x)) + (L /. (J . y))) by A27;

        (L /. (J . x)) = (L1 . x) by Lm1, A28, FUNCT_1: 12;

        hence (L1 . (x + y)) = ((L1 . x) + (L1 . y)) by Lm1, A28, A30, FUNCT_1: 12;

      end;

      now

        let x be Point of ( REAL-NS 1), a be Real;

        (L1 . (a * x)) = (L /. (J . (a * x))) by Lm1, A28, FUNCT_1: 12;

        then (L1 . (a * x)) = (L /. (a * (J . x))) by A1, PDIFF_1: 4;

        then (L1 . (a * x)) = ((a * (J . x)) * r) by A27;

        then

         A31: (L1 . (a * x)) = (a * ((J . x) * r)) by RLVECT_1:def 7;

        (L /. (J . x)) = (L1 . x) by Lm1, A28, FUNCT_1: 12;

        hence (L1 . (a * x)) = (a * (L1 . x)) by A31, A27;

      end;

      then

      reconsider L1 as LinearOperator of ( REAL-NS 1), Y by A29, LOPBAN_1:def 5, VECTSP_1:def 20;

      now

        let x be Point of ( REAL-NS 1);

         ||.(L1 . x).|| = ||.(L /. (J . x)).|| by Lm1, A28, FUNCT_1: 12;

        then ||.(L1 . x).|| = ||.((J . x) * r).|| by A27;

        then ||.(L1 . x).|| = ( ||.r.|| * |.(J . x).|) by NORMSP_1:def 1;

        hence ||.(L1 . x).|| <= (K * ||.x.||) by A1, PDIFF_1: 4;

      end;

      hence thesis by LOPBAN_1:def 8;

    end;

    theorem :: ORDEQ_02:5

    

     FTh42: for I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y st I = (( proj (1,1)) qua Function " ) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & (f * I) = g & f is_differentiable_in x0 holds g is_differentiable_in y0 & ( diff (g,y0)) = (( diff (f,x0)) . <*1*>) & for r be Element of REAL holds (( diff (f,x0)) . <*r*>) = (r * ( diff (g,y0)))

    proof

      let I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y;

      assume that

       A1: I = (( proj (1,1)) qua Function " ) and

       A2: x0 in ( dom f) and

       A3: y0 in ( dom g) and

       A4: x0 = <*y0*> and

       A5: (f * I) = g and

       A6: f is_differentiable_in x0;

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

      consider NN be Neighbourhood of x0 such that

       A7: NN c= ( dom f) and

       A8: ex L be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),Y)), R be RestFunc of ( REAL-NS 1), Y st for x be Point of ( REAL-NS 1) st x in NN holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A6;

      

       A9: (I * J) = ( id ( REAL-NS 1)) by Lm1, A1, Lm2, FUNCT_1: 39;

      

       A10: (g * J) = (f * ( id ( REAL-NS 1))) by A9, A5, RELAT_1: 36

      .= f by FUNCT_2: 17;

      consider e be Real such that

       A11: 0 < e and

       A12: { z where z be Point of ( REAL-NS 1) : ||.(z - x0).|| < e } c= NN by NFCONT_1:def 1;

      consider L be Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),Y)), R be RestFunc of ( REAL-NS 1), Y such that

       A13: for x9 be Point of ( REAL-NS 1) st x9 in NN holds ((f /. x9) - (f /. x0)) = ((L . (x9 - x0)) + (R /. (x9 - x0))) by A8;

      reconsider R0 = (R * I) as RestFunc of Y by A1, FTh40;

      L is LinearOperator of ( REAL-NS 1), Y by LOPBAN_1:def 9;

      then

      reconsider L0 = (L * I) as LinearFunc of Y by A1, FTh40;

      set N = { z where z be Point of ( REAL-NS 1) : ||.(z - x0).|| < e };

      

       A14: N c= the carrier of ( REAL-NS 1)

      proof

        let y be object;

        assume y in N;

        then ex z be Point of ( REAL-NS 1) st y = z & ||.(z - x0).|| < e;

        hence thesis;

      end;

      then

      reconsider N as Neighbourhood of x0 by A11, NFCONT_1:def 1;

      set N0 = { z where z be Element of REAL : |.(z - y0).| < e };

      now

        let z be object;

        hereby

          assume z in N0;

          then

          consider y9 be Element of REAL such that

           A16: z = y9 and

           A17: |.(y9 - y0).| < e;

          reconsider w = (I . y9) as Point of ( REAL-NS 1);

          x0 = (I . y0) by A1, A4, Lm2;

          then (w - x0) = (I . (y9 - y0)) by A1, Lm1, PDIFF_1: 3;

          then ||.(w - x0).|| = |.(y9 - y0).| by A1, Lm1, PDIFF_1: 3;

          then

           A18: w in { z0 where z0 be Point of ( REAL-NS 1) : ||.(z0 - x0).|| < e } by A17;

          (J . (I . y9)) = y9 by A1, Lm2, FUNCT_1: 35;

          hence z in (J .: N) by A18, A16, FUNCT_2: 35;

        end;

        assume z in (J .: N);

        then

        consider ww be object such that

         A19: ww in ( REAL 1) & ww in N & z = (J . ww) by FUNCT_2: 64;

        consider w be Point of ( REAL-NS 1) such that

         A21: ww = w & ||.(w - x0).|| < e by A19;

        reconsider y9 = (J . w) as Element of REAL ;

        (J . x0) = y0 by A4, Lm2;

        then (J . (w - x0)) = (y9 - y0) by PDIFF_1: 4;

        then |.(y9 - y0).| < e by A21, PDIFF_1: 4;

        hence z in N0 by A19, A21;

      end;

      then

       A23: N0 = (J .: N) by TARSKI: 2;

      (J .: ( dom f)) = (J .: (J " ( dom g))) by A10, RELAT_1: 147;

      then

       A24: (J .: ( dom f)) = ( dom (f * I)) by A5, Lm2, FUNCT_1: 77;

      

       A25: (I * J) = ( id ( REAL 1)) by A1, Lm2, FUNCT_1: 39;

      

       A261: N c= ( dom f) by A7, A12;

      then

       A26: N0 c= ( dom (f * I)) by A24, A23, RELAT_1: 123;

      

       A27: ].(y0 - e), (y0 + e).[ c= N0

      proof

        now

          let d be object;

          assume

           A28: d in ].(y0 - e), (y0 + e).[;

          then

          reconsider y1 = d as Element of REAL ;

           |.(y1 - y0).| < e by A28, RCOMP_1: 1;

          hence d in N0;

        end;

        hence thesis;

      end;

      N0 c= ].(y0 - e), (y0 + e).[

      proof

        let d be object;

        assume d in N0;

        then ex r be Element of REAL st d = r & |.(r - y0).| < e;

        hence thesis by RCOMP_1: 1;

      end;

      then N0 = ].(y0 - e), (y0 + e).[ by A27, XBOOLE_0:def 10;

      then

       A29: N0 is Neighbourhood of y0 by A11, RCOMP_1:def 6;

      N c= ( REAL 1) by A14, REAL_NS1:def 4;

      then ((I * J) .: N) = N by A25, FRECHET: 13;

      then

       A30: (I .: N0) = N by A23, RELAT_1: 126;

      

       A31: for y1 be Real st y1 in N0 holds (((f * I) /. y1) - ((f * I) /. y0)) = ((L0 /. (y1 - y0)) + (R0 /. (y1 - y0)))

      proof

        let y1 be Real;

        reconsider yy = y1 as Element of REAL by XREAL_0:def 1;

        reconsider y9 = (I . yy) as Point of ( REAL-NS 1);

        R is total by NDIFF_1:def 5;

        then

         A32: ( dom R) = the carrier of ( REAL-NS 1) by PARTFUN1:def 2;

        R0 is total by NDIFF_3:def 1;

        then

         A33: ( dom (R * I)) = REAL by PARTFUN1:def 2;

        reconsider dy1y0 = (y1 - y0) as Element of REAL by XREAL_0:def 1;

        (I . dy1y0) in ( dom R) by A32;

        then (R /. (I . (y1 - y0))) = (R . (I . (y1 - y0))) by PARTFUN1:def 6;

        then (R /. (I . dy1y0)) = (R0 . dy1y0) by A33, FUNCT_1: 12;

        then

         A34: (R /. (I . (y1 - y0))) = (R0 /. dy1y0) by A33, PARTFUN1:def 6;

        L0 is total;

        then

         A35: ( dom (L * I)) = REAL by PARTFUN1:def 2;

        assume

         A36: y1 in N0;

        then

         A37: (I . yy) in N by A30, FUNCT_2: 35;

        then (f /. (I . y1)) = (f . (I . y1)) by A7, A12, PARTFUN1:def 6;

        then (f /. (I . y1)) = ((f * I) . y1) by A26, A36, FUNCT_1: 12;

        then

         A39: (f /. (I . y1)) = ((f * I) /. y1) by A26, A36, PARTFUN1:def 6;

        

         A40: x0 = (I . y0) by A4, A1, Lm2;

        then (f /. (I . y0)) = (f . (I . y0)) by A2, PARTFUN1:def 6;

        then (f /. (I . y0)) = ((f * I) . y0) by A3, A5, FUNCT_1: 12;

        then

         A41: (f /. (I . y0)) = ((f * I) /. y0) by A3, A5, PARTFUN1:def 6;

        reconsider d = (y1 - y0) as Element of REAL by XREAL_0:def 1;

        ((f /. y9) - (f /. x0)) = ((L . (y9 - x0)) + (R /. (y9 - x0))) by A13, A12, A37;

        then

         A42: ((f /. (I . y1)) - (f /. (I . y0))) = ((L . (I . d)) + (R /. (y9 - x0))) by A1, A40, Lm1, PDIFF_1: 3;

        (L . (I . d)) = (L0 /. dy1y0) by A35, FUNCT_1: 12;

        hence thesis by A40, A42, A34, A39, A41, A1, Lm1, PDIFF_1: 3;

      end;

      hence g is_differentiable_in y0 by A5, A29, A261, A24, A23, RELAT_1: 123;

      then ( diff ((f * I),y0)) = (L0 /. jj) by A5, A31, A29, A26, NDIFF_3:def 4;

      

      hence

       A45: ( diff (g,y0)) = ((( diff (f,x0)) * I) . 1) by A5, A6, A13, A7, NDIFF_1:def 7

      .= (( diff (f,x0)) . (I . jj)) by A1, FUNCT_1: 13, PDIFF_1: 2

      .= (( diff (f,x0)) . <*1*>) by A1, Lm2;

      let r be Element of REAL ;

      

       A46: <*jj*> is Element of ( REAL 1) by FINSEQ_2: 98;

      then

      reconsider x = <*1*> as Point of ( REAL-NS 1) by REAL_NS1:def 4;

      

       A47: ( diff (f,x0)) is LinearOperator of ( REAL-NS 1), Y by LOPBAN_1:def 9;

      

      thus (( diff (f,x0)) . <*r*>) = (( diff (f,x0)) . <*(r * 1)*>)

      .= (( diff (f,x0)) . (r * <*1*>)) by RVSUM_1: 47

      .= (( diff (f,x0)) . (r * x)) by A46, REAL_NS1: 3

      .= (r * ( diff (g,y0))) by A45, A47, LOPBAN_1:def 5;

    end;

    theorem :: ORDEQ_02:6

    

     FTh43: for I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Real, g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y st I = (( proj (1,1)) qua Function " ) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & (f * I) = g holds f is_differentiable_in x0 iff g is_differentiable_in y0

    proof

      let I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Real, g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y;

      assume that

       A1: I = (( proj (1,1)) qua Function " ) and

       A2: x0 in ( dom f) and

       A3: y0 in ( dom g) and

       A4: x0 = <*y0*> and

       A5: (f * I) = g;

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

      thus f is_differentiable_in x0 implies g is_differentiable_in y0 by A2, A3, A4, A5, FTh42, A1;

      assume g is_differentiable_in y0;

      then

      consider N0 be Neighbourhood of y0 such that

       A6: N0 c= ( dom (f * I)) and

       A7: ex L be LinearFunc of Y, R be RestFunc of Y st for y be Real st y in N0 holds (((f * I) /. y) - ((f * I) /. y0)) = ((L /. (y - y0)) + (R /. (y - y0))) by A5;

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

      

       A8: (I * J) = ( id ( REAL-NS 1)) by Lm1, A1, Lm2, FUNCT_1: 39;

      

       A9: (g * J) = (f * ( id ( REAL-NS 1))) by A5, A8, RELAT_1: 36

      .= f by FUNCT_2: 17;

      consider e0 be Real such that

       A10: 0 < e0 and

       A11: N0 = ].(y0 - e0), (y0 + e0).[ by RCOMP_1:def 6;

      reconsider e = e0 as Element of REAL by XREAL_0:def 1;

      set N = { z where z be Point of ( REAL-NS 1) : ||.(z - x0).|| < e };

      consider L be LinearFunc of Y, R be RestFunc of Y such that

       A12: for y1 be Real st y1 in N0 holds (((f * I) /. y1) - ((f * I) /. y0)) = ((L /. (y1 - y0)) + (R /. (y1 - y0))) by A7;

      reconsider R0 = (R * J) as RestFunc of ( REAL-NS 1), Y by FTh41;

      reconsider L0 = (L * J) as Lipschitzian LinearOperator of ( REAL-NS 1), Y by FTh41;

      now

        let z be object;

        hereby

          assume z in N;

          then

          consider w be Point of ( REAL-NS 1) such that

           A13: z = w and

           A14: ||.(w - x0).|| < e;

          reconsider y2 = (J . w) as Element of REAL ;

          (J . x0) = y0 by A4, Lm2;

          then (J . (w - x0)) = (y2 - y0) by PDIFF_1: 4;

          then |.(y2 - y0).| < e by A14, PDIFF_1: 4;

          then

           A15: y2 in N0 by A11, RCOMP_1: 1;

          w in the carrier of ( REAL-NS 1);

          then w in ( dom J) by Lm2, REAL_NS1:def 4;

          then w = (I . y2) by A1, FUNCT_1: 34;

          hence z in (I .: N0) by A13, A15, FUNCT_2: 35;

        end;

        assume z in (I .: N0);

        then

        consider yy be object such that

         A16: yy in REAL and

         A17: yy in N0 and

         A18: z = (I . yy) by FUNCT_2: 64;

        reconsider y3 = yy as Element of REAL by A16;

        set w = (I . y3);

        (I . y0) = x0 by A4, A1, Lm2;

        then

         A19: (w - x0) = (I . (y3 - y0)) by A1, Lm1, PDIFF_1: 3;

         |.(y3 - y0).| < e by A11, A17, RCOMP_1: 1;

        then ||.(w - x0).|| < e by A19, A1, Lm1, PDIFF_1: 3;

        hence z in N by A18;

      end;

      then

       A20: N = (I .: N0) by TARSKI: 2;

      (I .: ( dom g)) = (I .: (I " ( dom f))) by A5, RELAT_1: 147;

      then

       A211: (I .: ( dom g)) = ( dom f) by A1, Lm1, FUNCT_1: 77, PDIFF_1: 2;

      then

       A21: N c= ( dom f) by A5, A6, A20, RELAT_1: 123;

      N c= the carrier of ( REAL-NS 1)

      proof

        let y be object;

        assume y in N;

        then ex z be Point of ( REAL-NS 1) st y = z & ||.(z - x0).|| < e;

        hence thesis;

      end;

      then

       A22: N is Neighbourhood of x0 by A10, NFCONT_1:def 1;

      (J * I) = ( id REAL ) by A1, Lm2, FUNCT_1: 39;

      then ((J * I) .: N0) = N0 by FRECHET: 13;

      then

       A23: (J .: N) = N0 by A20, RELAT_1: 126;

      

       A24: for y be Point of ( REAL-NS 1) st y in N holds ((f /. y) - (f /. x0)) = ((L0 . (y - x0)) + (R0 /. (y - x0)))

      proof

        x0 in the carrier of ( REAL-NS 1);

        then x0 in ( dom J) by Lm2, REAL_NS1:def 4;

        then (g . (J . x0)) = (f . x0) by A9, FUNCT_1: 13;

        then

         A25: (g . (J . x0)) = (f /. x0) by A2, PARTFUN1:def 6;

        

         A26: (J . x0) = y0 by A4, Lm2;

        let y be Point of ( REAL-NS 1);

        assume

         A27: y in N;

        set y3 = (J . y);

        reconsider p1 = (g /. y3), p2 = (g /. y0), q1 = (L /. (y3 - y0)), q2 = (R /. (y3 - y0)) as VECTOR of Y;

        

         A28: (J . x0) = y0 by A4, Lm2;

        ((g /. y3) - (g /. y0)) = (q1 + q2) by A5, A12, A23, A27, FUNCT_2: 35;

        then ((g /. (J . y)) - (g /. (J . x0))) = ((L /. (J . (y - x0))) + (R /. (y3 - y0))) by A28, PDIFF_1: 4;

        then

         A29: ((g /. (J . y)) - (g /. (J . x0))) = ((L /. (J . (y - x0))) + (R /. (J . (y - x0)))) by A28, PDIFF_1: 4;

        

         A30: ( dom L0) = the carrier of ( REAL-NS 1) by FUNCT_2:def 1;

        (y - x0) in the carrier of ( REAL-NS 1);

        then (y - x0) in ( dom J) by Lm2, REAL_NS1:def 4;

        then

         A31: (R . (J . (y - x0))) = ((R * J) . (y - x0)) by FUNCT_1: 13;

        R0 is total by NDIFF_1:def 5;

        then

         A32: ( dom (R * J)) = the carrier of ( REAL-NS 1) by PARTFUN1:def 2;

        

         A33: (R . (J . (y - x0))) = (R0 /. (y - x0)) by A31, A32, PARTFUN1:def 6;

        (J . (y - x0)) in ( dom R) by A32, FUNCT_1: 11;

        then

         A34: (R /. (J . (y - x0))) = (R0 /. (y - x0)) by A33, PARTFUN1:def 6;

        y in the carrier of ( REAL-NS 1);

        then

         A35: y in ( dom J) by Lm2, REAL_NS1:def 4;

        (g . (J . y)) = (f . y) by A9, A35, FUNCT_1: 13;

        then

         A36: (g . (J . y)) = (f /. y) by A21, A27, PARTFUN1:def 6;

        (J . y) in ( dom g) by A21, A27, A9, FUNCT_1: 11;

        then (g /. (J . y)) = (f /. y) by A36, PARTFUN1:def 6;

        then ((g /. (J . y)) - (g /. (J . x0))) = ((f /. y) - (f /. x0)) by A3, A26, A25, PARTFUN1:def 6;

        hence thesis by A29, A34, A30, FUNCT_1: 12;

      end;

      reconsider L0 as Point of ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS 1),Y)) by LOPBAN_1:def 9;

      for x be Point of ( REAL-NS 1) st x in N holds ((f /. x) - (f /. x0)) = ((L0 . (x - x0)) + (R0 /. (x - x0))) by A24;

      hence f is_differentiable_in x0 by A22, A211, A5, A6, A20, RELAT_1: 123;

    end;

    theorem :: ORDEQ_02:7

    

     FTh44: for J be Function of ( REAL-NS 1), REAL , x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y st J = ( proj (1,1)) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & f = (g * J) holds f is_differentiable_in x0 iff g is_differentiable_in y0

    proof

      let J be Function of ( REAL-NS 1), REAL , x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y;

      assume

       A1: J = ( proj (1,1)) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & f = (g * J);

      reconsider I = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL-NS 1) by PDIFF_1: 2, REAL_NS1:def 4;

      (J * I) = ( id REAL ) by A1, Lm2, FUNCT_1: 39;

      

      then (f * I) = (g * ( id REAL )) by A1, RELAT_1: 36

      .= g by FUNCT_2: 17;

      hence thesis by A1, FTh43;

    end;

    

     LM519A: for x be Point of ( REAL-NS 1) holds ex z be Real st x = <*z*>

    proof

      let x be Point of ( REAL-NS 1);

      x is Element of ( REAL 1) by REAL_NS1:def 4;

      then ex z be Element of REAL st x = <*z*> by FINSEQ_2: 97;

      hence thesis;

    end;

    theorem :: ORDEQ_02:8

    

     FTh42A: for I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y st I = (( proj (1,1)) qua Function " ) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & (f * I) = g & f is_differentiable_in x0 holds ||.( diff (g,y0)).|| = ||.( diff (f,x0)).||

    proof

      let I be Function of REAL , ( REAL-NS 1), x0 be Point of ( REAL-NS 1), y0 be Element of REAL , g be PartFunc of REAL , Y, f be PartFunc of ( REAL-NS 1), Y;

      assume

       A1: I = (( proj (1,1)) qua Function " ) & x0 in ( dom f) & y0 in ( dom g) & x0 = <*y0*> & (f * I) = g & f is_differentiable_in x0;

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

      reconsider j1 = 1 as Real;

       <*jj*> in ( REAL 1) by FINSEQ_2: 98;

      then

      reconsider t = <*jj*> as Point of ( REAL-NS 1) by REAL_NS1:def 4;

      (J . t) = jj by Lm2;

      then ||.t.|| = |.j1.| by PDIFF_1: 4;

      then

       A3: ||.t.|| = 1 by ABSVALUE:def 1;

      reconsider dfx0 = ( diff (f,x0)) as Lipschitzian LinearOperator of ( REAL-NS 1), Y by LOPBAN_1:def 9;

      set A = ( PreNorms dfx0);

       ||.( diff (g,y0)).|| = ||.(( diff (f,x0)) . t).|| by A1, FTh42;

      then

       A5: ||.( diff (g,y0)).|| in A by A3;

      

       A6: ||.( diff (f,x0)).|| = ( upper_bound ( PreNorms ( modetrans (( diff (f,x0)),( REAL-NS 1),Y)))) by LOPBAN_1:def 13

      .= ( upper_bound A) by LOPBAN_1: 29;

      A is bounded_above by LOPBAN_1: 27;

      then

       A7: ||.( diff (g,y0)).|| <= ||.( diff (f,x0)).|| by A6, A5, SEQ_4:def 1;

      for r be Real st r in A holds r <= ||.( diff (g,y0)).||

      proof

        let r be Real;

        assume r in A;

        then

        consider v be VECTOR of ( REAL-NS 1) such that

         A8: r = ||.(dfx0 . v).|| & ||.v.|| <= 1;

        consider s be Real such that

         X12: v = <*s*> by LM519A;

        reconsider J = ( proj (1,1)) as Function of ( REAL 1), REAL ;

        (J . v) = s by X12, PDIFF_1: 1;

        then

         X13: ||.v.|| = |.s.| by PDIFF_1: 4;

        reconsider s1 = s as Element of REAL by XREAL_0:def 1;

        

         A9: (( diff (f,x0)) . <*s1*>) = (s1 * ( diff (g,y0))) by A1, FTh42;

        ( |.s.| * ||.( diff (g,y0)).||) <= (1 * ||.( diff (g,y0)).||) by A8, X13, XREAL_1: 64;

        hence thesis by A8, A9, X12, NORMSP_1:def 1;

      end;

      then ||.( diff (f,x0)).|| <= ||.( diff (g,y0)).|| by A6, SEQ_4: 45;

      hence ||.( diff (g,y0)).|| = ||.( diff (f,x0)).|| by A7, XXREAL_0: 1;

    end;

    theorem :: ORDEQ_02:9

    

     LM519B1: for a,b,z be Real, p,q,x be Point of ( REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds (z in ].a, b.[ implies x in ].p, q.[) & (x in ].p, q.[ implies a <> b & (a < b implies z in ].a, b.[) & (a > b implies z in ].b, a.[))

    proof

      let a,b,z be Real, p,q,x be Point of ( REAL-NS 1);

      reconsider I = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL 1) by PDIFF_1: 2;

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

      assume

       P2: p = <*a*> & q = <*b*> & x = <*z*>;

      

       A2: (I . a) = p & (I . b) = q & (I . z) = x & (J . p) = a & (J . q) = b & (J . x) = z by P2, PDIFF_1: 1;

      hereby

        assume z in ].a, b.[;

        then

         A4: a < z & z < b by XXREAL_1: 4;

        then

         A5: a < b by XXREAL_0: 2;

        reconsider r = ((z - a) / (b - a)) as Real;

        

         A6: 0 < (z - a) & 0 < (b - a) & (z - a) < (b - a) by A4, A5, XREAL_1: 14, XREAL_1: 50;

        then

         C1: 0 < r & r < 1 by XREAL_1: 139, XREAL_1: 191;

        

         C3: (((1 - r) * a) + (r * b)) = (a + (((z - a) / (b - a)) * (b - a)))

        .= (a + (z - a)) by A6, XCMPLX_1: 87;

        (q - p) = (I . (b - a)) by A2, PDIFF_1: 3;

        then (r * (q - p)) = (I . (r * (b - a))) by PDIFF_1: 3;

        then (p + (r * (q - p))) = x by A2, C3, PDIFF_1: 3;

        then x in { (p + (t * (q - p))) where t be Real : 0 < t & t < 1 } by C1;

        hence x in ].p, q.[ by A4, P2, FINSEQ_1: 76, NDIFF_5: 16;

      end;

      assume x in ].p, q.[;

      then

       X1: x in [.p, q.] & not x in {p, q} by XBOOLE_0:def 5;

      then x in { (((1 - r) * p) + (r * q)) where r be Real : 0 <= r & r <= 1 } by RLTOPSP1:def 2;

      then

      consider r be Real such that

       B1: x = (((1 - r) * p) + (r * q)) & 0 <= r & r <= 1;

      

       B2: (J . x) = ((J . ((1 - r) * p)) + (J . (r * q))) by B1, PDIFF_1: 4

      .= (((1 - r) * (J . p)) + (J . (r * q))) by PDIFF_1: 4

      .= (((1 - r) * (J . p)) + (r * (J . q))) by PDIFF_1: 4;

      hence a <> b by A2, X1, TARSKI:def 2;

       X3:

      now

        assume r = 0 ;

        

        then x = (p + ( 0 qua Real * q)) by B1, RLVECT_1:def 8

        .= (p + ( 0. ( REAL-NS 1))) by RLVECT_1: 10;

        hence contradiction by X1, TARSKI:def 2;

      end;

      now

        assume r = 1;

        

        then x = (( 0 qua Real * p) + q) by B1, RLVECT_1:def 8

        .= (( 0. ( REAL-NS 1)) + q) by RLVECT_1: 10;

        hence contradiction by X1, TARSKI:def 2;

      end;

      then

       X4: r < 1 by B1, XXREAL_0: 1;

      set s = (1 - r);

      

       X5: r = (1 - s) & 0 < s & s < 1 by X3, B1, X4, XREAL_1: 44, XREAL_1: 50;

      hereby

        assume a < b;

        then a < z & z < b by A2, X3, B1, X4, XREAL_1: 177, XREAL_1: 178, B2;

        hence z in ].a, b.[;

      end;

      assume a > b;

      then b < z & z < a by A2, X5, XREAL_1: 177, XREAL_1: 178, B2;

      hence z in ].b, a.[;

    end;

    theorem :: ORDEQ_02:10

    

     LM519C1: for a,b,z be Real, p,q,x be Point of ( REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds (z in [.a, b.] implies x in [.p, q.]) & (x in [.p, q.] implies (a <= b implies z in [.a, b.]) & (a >= b implies z in [.b, a.]))

    proof

      let a,b,z be Real, p,q,x be Point of ( REAL-NS 1);

      reconsider I = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL 1) by PDIFF_1: 2;

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

      assume

       A1: p = <*a*> & q = <*b*> & x = <*z*>;

      then

       A2: p = (I . a) & q = (I . b) & x = (I . z) & (J . p) = a & (J . q) = b & (J . x) = z by PDIFF_1: 1;

      thus z in [.a, b.] implies x in [.p, q.]

      proof

        assume z in [.a, b.];

        then

         A5: a <= z & z <= b by XXREAL_1: 1;

        then

         A6: a <= b by XXREAL_0: 2;

        per cases ;

          suppose

           Z1: a = b;

          reconsider r = 0 as Real;

          

           Z2: z = (((1 - r) * a) + (r * b)) by Z1, A5, XXREAL_0: 1;

          ((1 - r) * p) = (I . ((1 - r) * a)) & (r * q) = (I . (r * b)) by A2, PDIFF_1: 3;

          then (I . z) = (((1 - r) * p) + (r * q)) by Z2, PDIFF_1: 3;

          then x = (((1 - r) * p) + (r * q)) by A1, PDIFF_1: 1;

          then x in { (((1 - r) * p) + (r * q)) where r be Real : 0 <= r & r <= 1 };

          hence thesis by RLTOPSP1:def 2;

        end;

          suppose a <> b;

          then

           X2: a < b by A6, XXREAL_0: 1;

          reconsider r = ((z - a) / (b - a)) as Real;

          

           A7: 0 <= (z - a) & 0 <= (b - a) by A5, A6, XREAL_1: 48;

          (z - a) <= (b - a) by A5, XREAL_1: 13;

          then

           C2: r <= 1 by A7, XREAL_1: 185;

          

           A8: 0 < (b - a) by X2, XREAL_1: 50;

          

           C3: (((1 - r) * a) + (r * b)) = (a + (((z - a) / (b - a)) * (b - a)))

          .= (a + (z - a)) by A8, XCMPLX_1: 87;

          ((1 - r) * p) = (I . ((1 - r) * a)) & (r * q) = (I . (r * b)) by A2, PDIFF_1: 3;

          

          then (((1 - r) * p) + (r * q)) = (I . z) by C3, PDIFF_1: 3

          .= x by A1, PDIFF_1: 1;

          then x in { (((1 - r) * p) + (r * q)) where r be Real : 0 <= r & r <= 1 } by A7, C2;

          hence thesis by RLTOPSP1:def 2;

        end;

      end;

      assume x in [.p, q.];

      then x in { (((1 - r) * p) + (r * q)) where r be Real : 0 <= r & r <= 1 } by RLTOPSP1:def 2;

      then

      consider r be Real such that

       B2: x = (((1 - r) * p) + (r * q)) & 0 <= r & r <= 1;

      

       B4: (J . x) = ((J . ((1 - r) * p)) + (J . (r * q))) by B2, PDIFF_1: 4

      .= (((1 - r) * (J . p)) + (J . (r * q))) by PDIFF_1: 4

      .= (((1 - r) * (J . p)) + (r * (J . q))) by PDIFF_1: 4;

       B5:

      now

        assume a <= b;

        then a <= z & z <= b by A2, XREAL_1: 171, XREAL_1: 172, B2, B4;

        hence z in [.a, b.];

      end;

      now

        assume

         B6: a >= b;

        set s = (1 - r);

         0 <= s & s <= 1 & (J . x) = ((s * (J . p)) + ((1 - s) * (J . q))) by B2, B4, XREAL_1: 43, XREAL_1: 48;

        then b <= z & z <= a by A2, XREAL_1: 171, XREAL_1: 172, B6;

        hence z in [.b, a.];

      end;

      hence thesis by B5;

    end;

    theorem :: ORDEQ_02:11

    

     LM519D: for a,b be Real, p,q be Point of ( REAL-NS 1), I be Function of REAL , ( REAL-NS 1) st p = <*a*> & q = <*b*> & I = (( proj (1,1)) qua Function " ) holds (a <= b implies (I .: [.a, b.]) = [.p, q.]) & (a < b implies (I .: ].a, b.[) = ].p, q.[)

    proof

      let a,b be Real, p,q be Point of ( REAL-NS 1), I be Function of REAL , ( REAL-NS 1);

      assume that

       A1: p = <*a*> & q = <*b*> and

       A2: I = (( proj (1,1)) qua Function " );

      hereby

        assume

         X1: a <= b;

        now

          let y be object;

          assume y in (I .: [.a, b.]);

          then

          consider x be object such that

           A3: x in ( dom I) & [x, y] in I & x in [.a, b.] by RELAT_1: 110;

          reconsider x as Element of REAL by A3;

          (I . x) = <*x*> by A2, PDIFF_1: 1;

          then (I . x) in [.p, q.] by A1, A3, LM519C1;

          hence y in [.p, q.] by A3, FUNCT_1: 1;

        end;

        then

         A6: (I .: [.a, b.]) c= [.p, q.];

        reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

        

         A7: (J . p) = a & (J . q) = b by A1, PDIFF_1: 1;

        now

          let x be object;

          assume

           B0: x in [.p, q.];

          then x in { (((1 - r) * p) + (r * q)) where r be Real : 0 <= r & r <= 1 } by RLTOPSP1:def 2;

          then

          consider r be Real such that

           B2: x = (((1 - r) * p) + (r * q)) & 0 <= r & r <= 1;

          (J . x) = ((J . ((1 - r) * p)) + (J . (r * q))) by B2, PDIFF_1: 4

          .= (((1 - r) * (J . p)) + (J . (r * q))) by PDIFF_1: 4

          .= (((1 - r) * (J . p)) + (r * (J . q))) by PDIFF_1: 4;

          then a <= (J . x) & (J . x) <= b by A7, X1, XREAL_1: 171, XREAL_1: 172, B2;

          then

           B5: (J . x) in [.a, b.];

          then

          reconsider z = (J . x) as Element of REAL ;

          set z1 = (I . z);

           [z, (I . z)] in I by A2, PDIFF_1: 2, FUNCT_1: 1;

          then

           B9: (I . z) in (I .: [.a, b.]) by B5, A2, PDIFF_1: 2, RELAT_1: 110;

          (I * J) = ( id ( rng I)) by PDIFF_1: 2, A2, Lm2, FUNCT_1: 39;

          then J = (I " ) by A2, PDIFF_1: 2, Lm2, FUNCT_1: 42;

          hence x in (I .: [.a, b.]) by B9, FUNCT_1: 35, Lm1, A2, PDIFF_1: 2, B0;

        end;

        then [.p, q.] c= (I .: [.a, b.]);

        hence (I .: [.a, b.]) = [.p, q.] by A6, XBOOLE_0:def 10;

      end;

      assume

       X2: a < b;

      now

        let y be object;

        assume y in (I .: ].a, b.[);

        then

        consider x be object such that

         B3: x in ( dom I) & [x, y] in I & x in ].a, b.[ by RELAT_1: 110;

        reconsider x as Element of REAL by B3;

        (I . x) = <*x*> by A2, PDIFF_1: 1;

        then (I . x) in ].p, q.[ by A1, B3, LM519B1;

        hence y in ].p, q.[ by B3, FUNCT_1: 1;

      end;

      then

       B6: (I .: ].a, b.[) c= ].p, q.[;

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL by Lm1;

      

       A7: (J . p) = a & (J . q) = b by A1, PDIFF_1: 1;

      now

        let x be object;

        assume

         B0: x in ].p, q.[;

        then

         B0c: x in [.p, q.] & not x in {p, q} by XBOOLE_0:def 5;

        then

         B0b: x <> p & x <> q by TARSKI:def 2;

        x in { (((1 - r) * p) + (r * q)) where r be Real : 0 <= r & r <= 1 } by B0c, RLTOPSP1:def 2;

        then

        consider r be Real such that

         B1: x = (((1 - r) * p) + (r * q)) & 0 <= r & r <= 1;

        now

          assume r = 1;

          then x = (( 0. ( REAL-NS 1)) + (1 qua Real * q)) by B1, RLVECT_1: 10;

          hence contradiction by B0b, RLVECT_1:def 8;

        end;

        then

         B1a: r < 1 by B1, XXREAL_0: 1;

         B1b:

        now

          assume r = 0 ;

          then x = ((1 qua Real * p) + ( 0. ( REAL-NS 1))) by B1, RLVECT_1: 10;

          hence contradiction by B0b, RLVECT_1:def 8;

        end;

        (J . x) = ((J . ((1 - r) * p)) + (J . (r * q))) by B1, PDIFF_1: 4

        .= (((1 - r) * (J . p)) + (J . (r * q))) by PDIFF_1: 4

        .= (((1 - r) * (J . p)) + (r * (J . q))) by PDIFF_1: 4;

        then a < (J . x) & (J . x) < b by A7, X2, XREAL_1: 177, XREAL_1: 178, B1a, B1, B1b;

        then

         B5: (J . x) in ].a, b.[;

        then

        reconsider z = (J . x) as Element of REAL ;

        set z1 = (I . z);

        

         B91: [z, (I . z)] in I by A2, PDIFF_1: 2, FUNCT_1: 1;

        

         B11: ( rng I) = the carrier of ( REAL-NS 1) by A2, REAL_NS1:def 4, PDIFF_1: 2;

        (I * J) = ( id ( rng I)) by PDIFF_1: 2, A2, Lm2, FUNCT_1: 39;

        then

         B14: J = (I " ) by A2, PDIFF_1: 2, Lm2, FUNCT_1: 42;

        x = (I . (J . x)) by A2, B14, FUNCT_1: 35, B11, B0;

        hence x in (I .: ].a, b.[) by B91, B5, A2, PDIFF_1: 2, RELAT_1: 110;

      end;

      then ].p, q.[ c= (I .: ].a, b.[);

      hence (I .: ].a, b.[) = ].p, q.[ by B6, XBOOLE_0:def 10;

    end;

    theorem :: ORDEQ_02:12

    

     Th519: for Y be RealNormSpace, g be PartFunc of REAL , the carrier of Y, a,b,M be Real st a <= b & [.a, b.] c= ( dom g) & (for x be Real st x in [.a, b.] holds g is_continuous_in x) & (for x be Real st x in ].a, b.[ holds g is_differentiable_in x) & (for x be Real st x in ].a, b.[ holds ||.( diff (g,x)).|| <= M) holds ||.((g /. b) - (g /. a)).|| <= (M * |.(b - a).|)

    proof

      let Y be RealNormSpace, g be PartFunc of REAL , the carrier of Y, a,b,M be Real;

      assume

       AS0: a <= b;

      assume

       AS1: [.a, b.] c= ( dom g);

      assume

       AS2: for x be Real st x in [.a, b.] holds g is_continuous_in x;

      assume

       AS3: for x be Real st x in ].a, b.[ holds g is_differentiable_in x;

      assume

       AS4: for x be Real st x in ].a, b.[ holds ||.( diff (g,x)).|| <= M;

      the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider J = ( proj (1,1)) as Function of ( REAL-NS 1), REAL ;

      reconsider f = (g * J) as PartFunc of ( REAL-NS 1), Y;

      reconsider I = (( proj (1,1)) qua Function " ) as Function of REAL , ( REAL-NS 1) by PDIFF_1: 2, REAL_NS1:def 4;

      now

        let r be Real;

        r is Element of REAL by XREAL_0:def 1;

        then <*r*> in ( REAL 1) by FINSEQ_2: 98;

        hence <*r*> is Point of ( REAL-NS 1) by REAL_NS1:def 4;

      end;

      then

      reconsider p = <*a*>, q = <*b*> as Point of ( REAL-NS 1);

      

       Y0: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

      

       DX1: (J * I) = ( id REAL ) by Lm2, FUNCT_1: 39;

      

       DX2: (f * I) = (g * ( id REAL )) by DX1, RELAT_1: 36

      .= g by FUNCT_2: 17;

      ( dom f) = (J " ( dom g)) by RELAT_1: 147

      .= (I .: ( dom g)) by FUNCT_1: 85;

      then (I .: [.a, b.]) c= ( dom f) by AS1, RELAT_1: 123;

      then

       X0: [.p, q.] c= ( dom f) by AS0, LM519D;

      

       X1: for x be Point of ( REAL-NS 1) st x in [.p, q.] holds f is_continuous_in x

      proof

        let x be Point of ( REAL-NS 1);

        assume

         X11: x in [.p, q.];

        consider z be Real such that

         X12: x = <*z*> by LM519A;

        z in [.a, b.] by AS0, LM519C1, X11, X12;

        then g is_continuous_in z by AS2;

        hence f is_continuous_in x by NDIFF435, X12, X0, X11;

      end;

      

       X2: for x be Point of ( REAL-NS 1) st x in ].p, q.[ holds f is_differentiable_in x

      proof

        let x be Point of ( REAL-NS 1);

        assume

         X11: x in ].p, q.[;

        then

         X15: x in [.p, q.] by XBOOLE_0:def 5;

        consider z be Real such that

         X12: x = <*z*> by LM519A;

        per cases ;

          suppose a = b;

          hence f is_differentiable_in x by X11, X12, LM519B1;

        end;

          suppose a <> b;

          then a < b by AS0, XXREAL_0: 1;

          then z in ].a, b.[ by LM519B1, X11, X12;

          then z in ( dom g) & g is_differentiable_in z by AS1, Y0, AS3;

          hence f is_differentiable_in x by FTh44, X12, X0, X15;

        end;

      end;

      

       X3: for x be Point of ( REAL-NS 1) st x in ].p, q.[ holds ||.( diff (f,x)).|| <= M

      proof

        let x be Point of ( REAL-NS 1);

        assume

         X11: x in ].p, q.[;

        then

         B11: x in [.p, q.] by XBOOLE_0:def 5;

        consider z be Real such that

         X12: x = <*z*> by LM519A;

        per cases ;

          suppose a = b;

          hence ||.( diff (f,x)).|| <= M by X11, X12, LM519B1;

        end;

          suppose a <> b;

          then a < b by AS0, XXREAL_0: 1;

          then

           X13: z in ].a, b.[ by LM519B1, X11, X12;

          then

           X14: ||.( diff (g,z)).|| <= M by AS4;

          f is_differentiable_in x by X2, X11;

          hence ||.( diff (f,x)).|| <= M by B11, Y0, X0, X12, DX2, X14, FTh42A, AS1, X13;

        end;

      end;

      

       S0: ( dom I) = REAL by FUNCT_2:def 1;

      

       S1: p = (I . a) & q = (I . b) by PDIFF_1: 1;

      

       S2: p in ( dom f) & q in ( dom f) by X0, RLTOPSP1: 68;

      a in [.a, b.] & b in [.a, b.] by AS0;

      then (g /. a) = (g . a) & (g /. b) = (g . b) by PARTFUN1:def 6, AS1;

      then (g /. a) = (f . (I . a)) & (g /. b) = (f . (I . b)) by DX2, FUNCT_1: 13, S0, XREAL_0:def 1;

      then

       S3: (g /. a) = (f /. p) & (g /. b) = (f /. q) by S1, S2, PARTFUN1:def 6;

      (q - p) = (I . (b - a)) by S1, Lm1, PDIFF_1: 3;

      then ||.(q - p).|| = |.(b - a).| by Lm1, PDIFF_1: 3;

      hence thesis by NDIFF_5: 19, X0, X1, X2, X3, S3;

    end;

    begin

    reserve X,Y for RealBanachSpace;

    reserve Z for open Subset of REAL ;

    reserve a,b,c,d,e,r,x0 for Real;

    reserve y0 for VECTOR of X;

    reserve G for Function of X, X;

    

     Lm13a: for f be continuous PartFunc of REAL , the carrier of Y st ( [.a, b.] c= ( dom f) & c in [.a, b.] & d in [.a, b.] & for x be Real st x in [.( min (c,d)), ( max (c,d)).] holds ||.(f /. x).|| <= e) holds ||.( integral (f,c,d)).|| <= (e * |.(d - c).|)

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      set A = ['( min (c,d)), ( max (c,d))'];

      assume that

       A1: [.a, b.] c= ( dom f) & c in [.a, b.] & d in [.a, b.] and

       A2: for x be Real st x in [.( min (c,d)), ( max (c,d)).] holds ||.(f /. x).|| <= e;

      

       X0: a <= c & c <= b by A1, XXREAL_1: 1;

      then

       X3: a <= b by XXREAL_0: 2;

      

       X1: [.a, b.] = ['a, b'] by X0, XXREAL_0: 2, INTEGRA5:def 3;

      ( rng ||.f.||) c= REAL ;

      then

       A3: ||.f.|| is Function of ( dom ||.f.||), REAL by FUNCT_2: 2;

      ( min (c,d)) <= c & c <= ( max (c,d)) by XXREAL_0: 17, XXREAL_0: 25;

      then

       X2: ['( min (c,d)), ( max (c,d))'] = [.( min (c,d)), ( max (c,d)).] by XXREAL_0: 2, INTEGRA5:def 3;

      ( dom ||.f.||) = ( dom f) by NORMSP_0:def 2;

      then

       A4: ['( min (c,d)), ( max (c,d))'] c= ( dom ||.f.||) by A1, X0, XXREAL_0: 2, X1, INTEGR19: 3;

      then

      reconsider g = ( ||.f.|| | A) as Function of A, REAL by A3, FUNCT_2: 32;

      

       A5: ( vol A) = |.(d - c).| by INTEGRA6: 6;

      

       A6: ||.f.|| is_integrable_on A by A1, X3, X1, INTEGR21: 22;

      consider h be Function of A, REAL such that

       A7: ( rng h) = {e} and

       A8: (h | A) is bounded by INTEGRA4: 5;

       A9:

      now

        let x be Real;

        assume

         A10: x in A;

        then (g . x) = ( ||.f.|| . x) by FUNCT_1: 49;

        then

         A11: (g . x) = ||.(f /. x).|| by A10, A4, NORMSP_0:def 3;

        (h . x) in {e} by A7, A10, FUNCT_2: 4;

        then (h . x) = e by TARSKI:def 1;

        hence (g . x) <= (h . x) by A11, A2, A10, X2;

      end;

      

       A12: ||.( integral (f,c,d)).|| <= ( integral ( ||.f.||,( min (c,d)),( max (c,d)))) by A1, X1, X3, INTEGR21: 22;

      ( min (c,d)) <= c & c <= ( max (c,d)) by XXREAL_0: 17, XXREAL_0: 25;

      then

       A13: ( integral ( ||.f.||,( min (c,d)),( max (c,d)))) = ( integral ( ||.f.||,A)) by INTEGRA5:def 4, XXREAL_0: 2;

      

       A14: (g | A) is bounded by A1, X1, X3, INTEGR21: 22;

      h is integrable & ( integral h) = (e * ( vol A)) by A7, INTEGRA4: 4;

      then ( integral ( ||.f.||,( min (c,d)),( max (c,d)))) <= (e * |.(d - c).|) by A13, A8, A9, A6, A14, A5, INTEGRA2: 34;

      hence thesis by A12, XXREAL_0: 2;

    end;

    

     Lm14a: for f be continuous PartFunc of REAL , the carrier of Y st (c <= d & [.a, b.] c= ( dom f) & c in [.a, b.] & d in [.a, b.] & for x be Real st x in [.c, d.] holds ||.(f /. x).|| <= e) holds ||.( integral (f,c,d)).|| <= (e * (d - c))

    proof

      let f be continuous PartFunc of REAL , the carrier of Y;

      assume that

       A2: c <= d and

       A3: [.a, b.] c= ( dom f) & c in [.a, b.] & d in [.a, b.] & for x be Real st x in [.c, d.] holds ||.(f /. x).|| <= e;

      

       A4: |.(d - c).| = (d - c) by ABSVALUE:def 1, A2, XREAL_1: 48;

      ( min (c,d)) = c & ( max (c,d)) = d by A2, XXREAL_0:def 9, XXREAL_0:def 10;

      hence thesis by A3, A4, Lm13a;

    end;

    

     Lm17: for X be RealNormSpace, x be Point of X holds ||.((a " ) * x).|| = ( ||.x.|| / |.a.|)

    proof

      let X be RealNormSpace, x be Point of X;

       ||.((a " ) * x).|| = ( |.(a " ).| * ||.x.||) by NORMSP_1:def 1;

      hence ||.((a " ) * x).|| = ( ||.x.|| / |.a.|) by COMPLEX1: 66;

    end;

    theorem :: ORDEQ_02:13

    

     Th1955: for X be RealBanachSpace, F be PartFunc of REAL , the carrier of X, f be continuous PartFunc of REAL , the carrier of X st [.a, b.] c= ( dom f) & ].a, b.[ c= ( dom F) & (for x be Real st x in ].a, b.[ holds (F /. x) = ( integral (f,a,x))) & x0 in ].a, b.[ & f is_continuous_in x0 holds F is_differentiable_in x0 & ( diff (F,x0)) = (f /. x0)

    proof

      let X be RealBanachSpace, F be PartFunc of REAL , the carrier of X, f be continuous PartFunc of REAL , the carrier of X;

      deffunc F2( object) = ( 0. X);

      assume that

       A4: [.a, b.] c= ( dom f) and

       A5: ].a, b.[ c= ( dom F) and

       A6: for x be Real st x in ].a, b.[ holds (F /. x) = ( integral (f,a,x)) and

       A7: x0 in ].a, b.[ and

       A8: f is_continuous_in x0;

      per cases ;

        suppose

         A1: a <= b;

        then

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

        defpred C1[ object] means (x0 + ( In ($1, REAL ))) in ].a, b.[;

        deffunc F0( Real) = ($1 * (f /. x0));

        consider L be Function of REAL , the carrier of X such that

         B9: for h be Element of REAL holds (L . h) = F0(h) from FUNCT_2:sch 4;

        

         A9: for h be Real holds (L . h) = F0(h)

        proof

          let h be Real;

          h is Element of REAL by XREAL_0:def 1;

          hence thesis by B9;

        end;

        

         C9: for h be Real holds (L /. h) = F0(h)

        proof

          let h be Real;

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

          (L /. h) = F0(h) by B9;

          hence thesis;

        end;

        then

        reconsider L as LinearFunc of X by NDIFF_3:def 2;

        deffunc F1( object) = (((F /. (x0 + ( In ($1, REAL )))) - (F /. x0)) - (L . ( In ($1, REAL ))));

        consider R be Function such that

         A10: ( dom R) = REAL & for x be object st x in REAL holds ( C1[x] implies (R . x) = F1(x)) & ( not C1[x] implies (R . x) = F2(x)) from PARTFUN1:sch 1;

        ( rng R) c= the carrier of X

        proof

          let y be object;

          assume y in ( rng R);

          then

          consider x be object such that

           A11: x in ( dom R) & y = (R . x) by FUNCT_1:def 3;

          ( C1[x] implies (R . x) = F1(x)) & ( not C1[x] implies (R . x) = F2(x)) by A10, A11;

          hence thesis by A11;

        end;

        then

        reconsider R as PartFunc of REAL , the carrier of X by A10, RELSET_1: 4;

        

         A14: R is total by A10, PARTFUN1:def 2;

        

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

        then

         X1: ].a, b.[ c= ['a, b'] by XXREAL_1: 25;

        

         A16: for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = ( 0. X)

        proof

          let h be 0 -convergent non-zero Real_Sequence;

          set Z0 = ( 0. X);

          

           A17: for e be Real st 0 < e holds ex n be Nat st for m be Nat st n <= m holds ||.((((h " ) (#) (R /* h)) . m) - Z0).|| < e

          proof

            set g = ( REAL --> (f /. x0));

            let e0 be Real;

            set e = (e0 / 2);

            

             A18: h is convergent & ( lim h) = 0 ;

            assume

             A19: 0 < e0;

            then

            consider p be Real such that

             A20: 0 < p and

             A21: for t be Real st t in ( dom f) & |.(t - x0).| < p holds ||.((f /. t) - (f /. x0)).|| < e by A8, NFCONT_3: 8, XREAL_1: 215;

            

             A22: (e0 / 2) < e0 & 0 < (p / 2) & (p / 2) < p by A19, A20, XREAL_1: 215, XREAL_1: 216;

            consider N be Neighbourhood of x0 such that

             A24: N c= ].a, b.[ by A7, RCOMP_1: 18;

            consider q be Real such that

             A25: 0 < q and

             A26: N = ].(x0 - q), (x0 + q).[ by RCOMP_1:def 6;

            set r = ( min ((p / 2),(q / 2)));

            

             A27: 0 < (q / 2) & (q / 2) < q by A25, XREAL_1: 215, XREAL_1: 216;

            then 0 < r by A22, XXREAL_0: 15;

            then

            consider n0 be Nat such that

             A28: for m be Nat st n0 <= m holds |.((h . m) - 0 ).| < r by A18, SEQ_2:def 7;

            reconsider n0 as Element of NAT by ORDINAL1:def 12;

            take n0;

            let m be Nat;

            

             A40: r <= (p / 2) & r <= (q / 2) by XXREAL_0: 17;

            then

             A29: ].(x0 - r), (x0 + r).[ c= ].(x0 - q), (x0 + q).[ by A27, INTEGRA6: 2, XXREAL_0: 2;

            assume n0 <= m;

            then

             A30: |.((h . m) - 0 ).| < r by A28;

            then |.((x0 + (h . m)) - x0).| < r;

            then

             A31: (x0 + (h . m)) in ].(x0 - q), (x0 + q).[ by A29, RCOMP_1: 1;

            then

             X2: (x0 + (h . m)) in ].a, b.[ by A24, A26;

            

             A32: (R . (h . m)) = (((F /. (x0 + (h . m))) - (F /. x0)) - (L . ( In ((h . m), REAL )))) by A10, A24, A26, A31;

            (F /. x0) = ( integral (f,a,x0)) & (F /. (x0 + (h . m))) = ( integral (f,a,(x0 + (h . m)))) by A6, A7, A24, A26, A31;

            then

             A35: (R . (h . m)) = ((( integral (f,a,(x0 + (h . m)))) - ( integral (f,a,x0))) - ((h . m) * (f /. x0))) by A9, A32;

            

             A36: ( dom g) = REAL ;

            ( ['a, b'] /\ ['a, b']) c= (( dom f) /\ ( dom g)) by A4, X5, XBOOLE_1: 27;

            then

             A37: ['a, b'] c= ( dom (f - g)) by VFUNCT_1:def 2;

            

             A39: ( integral (f,a,(x0 + (h . m)))) = (( integral (f,a,x0)) + ( integral (f,x0,(x0 + (h . m))))) by A1, X5, A4, A7, X1, X2, INTEGR21: 29;

            

             A41: for x be Real st x in ['( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m))))'] holds ||.((f - g) /. x).|| <= e

            proof

              let x be Real;

              

               A42: ( min (x0,(x0 + (h . m)))) <= x0 & x0 <= ( max (x0,(x0 + (h . m)))) by XXREAL_0: 17, XXREAL_0: 25;

              assume x in ['( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m))))'];

              then

               A43: x in [.( min (x0,(x0 + (h . m)))), ( max (x0,(x0 + (h . m)))).] by A42, INTEGRA5:def 3, XXREAL_0: 2;

               |.(x - x0).| <= |.(h . m).|

              proof

                per cases ;

                  suppose x0 <= (x0 + (h . m));

                  then x0 = ( min (x0,(x0 + (h . m)))) & (x0 + (h . m)) = ( max (x0,(x0 + (h . m)))) by XXREAL_0:def 9, XXREAL_0:def 10;

                  then

                   A44: ex z be Real st x = z & x0 <= z & z <= (x0 + (h . m)) by A43;

                  then

                   A45: |.(x - x0).| = (x - x0) by ABSVALUE:def 1, XREAL_1: 48;

                  

                   A46: (x - x0) <= ((x0 + (h . m)) - x0) by A44, XREAL_1: 9;

                  then 0 <= (h . m) by A44, XREAL_1: 48;

                  hence thesis by A46, A45, ABSVALUE:def 1;

                end;

                  suppose

                   A47: not x0 <= (x0 + (h . m));

                  then x0 = ( max (x0,(x0 + (h . m)))) & (x0 + (h . m)) = ( min (x0,(x0 + (h . m)))) by XXREAL_0:def 9, XXREAL_0:def 10;

                  then

                   A48: ex z be Real st x = z & (x0 + (h . m)) <= z & z <= x0 by A43;

                  then

                   A49: ((x0 + (h . m)) - x0) <= (x - x0) by XREAL_1: 9;

                  per cases ;

                    suppose (x - x0) <> 0 ;

                    then (x - x0) < 0 by A48, XREAL_1: 47;

                    then

                     A50: |.(x - x0).| = ( - (x - x0)) by ABSVALUE:def 1;

                     |.(h . m).| = ( - (h . m)) by A47, XREAL_1: 31, ABSVALUE:def 1;

                    hence thesis by A49, A50, XREAL_1: 24;

                  end;

                    suppose (x - x0) = 0 ;

                    then |.(x - x0).| = 0 by ABSVALUE:def 1;

                    hence thesis by COMPLEX1: 46;

                  end;

                end;

              end;

              then

               A52: |.(x - x0).| < r by A30, XXREAL_0: 2;

              then x in ].(x0 - q), (x0 + q).[ by A29, RCOMP_1: 1;

              then

               A53: x in [.a, b.] by X1, A15, A24, A26;

              reconsider xx = x as Element of REAL by XREAL_0:def 1;

               |.(x - x0).| < (p / 2) by A40, A52, XXREAL_0: 2;

              then |.(x - x0).| < p by A22, XXREAL_0: 2;

              then ||.((f /. x) - (f /. x0)).|| <= e by A4, A21, A53;

              then ||.((f /. x) - (g /. xx)).|| <= e;

              hence thesis by A15, A37, A53, VFUNCT_1:def 2;

            end;

             B54:

            now

              let x be Real;

              assume

               B1: x in ['a, b'];

              

              thus (g /. x) = (g . x) by A36, XREAL_0:def 1, PARTFUN1:def 6

              .= (f /. x0) by B1, FUNCOP_1: 7;

            end;

            

             XX: m in NAT by ORDINAL1:def 12;

            ( rng h) c= ( dom R) by A10;

            then (((h . m) " ) * (R /. (h . m))) = (((h . m) " ) * ((R /* h) . m)) by FUNCT_2: 109, XX;

            then (((h . m) " ) * (R /. (h . m))) = (((h " ) . m) * ((R /* h) . m)) by VALUED_1: 10;

            then

             A57: (((h . m) " ) * (R /. (h . m))) = (((h " ) (#) (R /* h)) . m) by NDIFF_1:def 2;

            

             A58: 0 < |.(h . m).| by COMPLEX1: 47, SEQ_1: 5;

            

             A60: ||.( integral ((f - g),x0,(x0 + (h . m)))).|| <= (e * |.((x0 + (h . m)) - x0).|) by A1, A7, X1, X2, A37, A41, INTEGR21: 25;

            

             A61: ( integral (g,x0,(x0 + (h . m)))) = (((x0 + (h . m)) - x0) * (f /. x0)) by A1, A7, X1, X2, A36, B54, INTEGR21: 28

            .= ((h . m) * (f /. x0));

            

             A62: ( integral ((f - g),x0,(x0 + (h . m)))) = (( integral (f,x0,(x0 + (h . m)))) - ( integral (g,x0,(x0 + (h . m))))) by A1, X5, A4, A7, X1, X2, A36, INTEGR21: 30;

            (R . (h . m)) = ((( integral (f,x0,(x0 + (h . m)))) + (( integral (f,a,x0)) - ( integral (f,a,x0)))) - ((h . m) * (f /. x0))) by A35, A39, RLVECT_1: 28

            .= ((( integral (f,x0,(x0 + (h . m)))) + Z0) - ((h . m) * (f /. x0))) by RLVECT_1: 15

            .= (( integral (f,x0,(x0 + (h . m)))) - ( integral (g,x0,(x0 + (h . m))))) by A61;

            then (R /. (h . m)) = ( integral ((f - g),x0,(x0 + (h . m)))) by A62, A10, PARTFUN1:def 6;

            then ||.(((h . m) " ) * (R /. (h . m))).|| = ( ||.(R /. (h . m)).|| / |.(h . m).|) & ( ||.(R /. (h . m)).|| / |.(h . m).|) <= ((e * |.(h . m).|) / |.(h . m).|) by A60, A58, Lm17, XREAL_1: 72;

            then ||.(((h . m) " ) * (R /. (h . m))).|| <= (e0 / 2) by A58, XCMPLX_1: 89;

            hence thesis by A22, A57, XXREAL_0: 2;

          end;

          hence ((h " ) (#) (R /* h)) is convergent;

          hence thesis by A17, NORMSP_1:def 7;

        end;

        consider N be Neighbourhood of x0 such that

         A64: N c= ].a, b.[ by A7, RCOMP_1: 18;

        reconsider R as RestFunc of X by A14, A16, NDIFF_3:def 1;

        

         A65: for x be Real st x in N holds ((F /. x) - (F /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

        proof

          let x be Real;

          assume x in N;

          then (x0 + ( In ((x - x0), REAL ))) = (x0 + (x - x0)) & (R . (x - x0)) = F1(-) by A10, A64;

          then (R /. (x - x0)) = (((F /. (x0 + ( In ((x - x0), REAL )))) - (F /. x0)) - (L /. ( In ((x - x0), REAL )))) by A10, PARTFUN1:def 6;

          then ((R /. (x - x0)) + (L /. (x - x0))) = (((F /. x) - (F /. x0)) - ((L /. (x - x0)) - (L /. (x - x0)))) by RLVECT_1: 29;

          then ((R /. (x - x0)) + (L /. (x - x0))) = (((F /. x) - (F /. x0)) - ( 0. X)) by RLVECT_1: 15;

          hence thesis;

        end;

        

         A66: N c= ( dom F) by A5, A64;

        hence

         A67: F is_differentiable_in x0 by A65;

        reconsider N1 = 1 as Real;

        (L /. 1) = (N1 * (f /. x0)) by C9;

        then (L /. 1) = (f /. x0) by RLVECT_1:def 8;

        hence thesis by A66, A65, A67, NDIFF_3:def 4;

      end;

        suppose a > b;

        hence thesis by A7, XXREAL_1: 28;

      end;

    end;

    theorem :: ORDEQ_02:14

    

     Th35: for F be PartFunc of REAL , the carrier of X, f be continuous PartFunc of REAL , the carrier of X st ( dom f) = [.a, b.] & ( dom F) = [.a, b.] & for t be Real st t in [.a, b.] holds (F /. t) = ( integral (f,a,t)) holds for x be Real st x in [.a, b.] holds F is_continuous_in x

    proof

      let F be PartFunc of REAL , the carrier of X;

      let f be continuous PartFunc of REAL , the carrier of X;

      set f1 = ||.f.||;

      assume

       A1: ( dom f) = [.a, b.] & ( dom F) = [.a, b.] & for t be Real st t in [.a, b.] holds (F /. t) = ( integral (f,a,t));

      let x0 be Real;

      assume

       A12: x0 in [.a, b.];

      per cases ;

        suppose a > b;

        hence thesis by A12, XXREAL_1: 29;

      end;

        suppose

         X1: a <= b;

        reconsider AB = ['a, b'] as non empty closed_interval Subset of REAL ;

        

         X2: AB = [.a, b.] by X1, INTEGRA5:def 3;

        then

         A2: (f | AB) is bounded by A1, X1, INTEGR21: 11;

        

         B1: ( dom f) = ( dom f1) by NORMSP_0:def 2;

        then (f1 | AB) = f1 by A1, X2;

        then f1 is bounded by A1, A2, X2, INTEGR21: 9;

        then

        consider K be Real such that

         A3: for y be set st y in ( dom f1) holds |.(f1 . y).| < K by COMSEQ_2:def 3;

        

         B2: [.a, b.] = AB by X1, INTEGRA5:def 3;

        then a in AB by X1;

        then |.(f1 . a).| < K by A1, X2, B1, A3;

        then

         A5: 0 < K by COMPLEX1: 46;

         A6:

        now

          let c,d be Real;

          assume

           A11: c in ['a, b'] & d in ['a, b'];

          then

           A7: ['( min (c,d)), ( max (c,d))'] c= ['a, b'] by X1, INTEGR19: 3;

          now

            let y be Real;

            assume y in ['( min (c,d)), ( max (c,d))'];

            then y in ['a, b'] by A7;

            then

             A9: y in ( dom f1) by X2, NORMSP_0:def 2, A1;

            then |.(f1 . y).| < K by A3;

            then |. ||.(f /. y).||.| < K by A9, NORMSP_0:def 2;

            hence ||.(f /. y).|| <= K by ABSVALUE:def 1;

          end;

          hence ||.( integral (f,c,d)).|| <= (K * |.(d - c).|) by A1, X1, X2, A11, INTEGR21: 25;

        end;

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom F) & |.(x1 - x0).| < s holds ||.((F /. x1) - (F /. x0)).|| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider s be Real such that

           A16: 0 < s & s < (r / K) by A5, XREAL_1: 5, XREAL_1: 139;

          (s * K) < ((r / K) * K) by A5, A16, XREAL_1: 68;

          then

           A17: (K * s) < r by A5, XCMPLX_1: 87;

          take s;

          thus 0 < s by A16;

          let x1 be Real;

          assume

           A18: x1 in ( dom F) & |.(x1 - x0).| < s;

          then

           A20: ||.( integral (f,x0,x1)).|| <= (K * |.(x1 - x0).|) by A1, A12, B2, A6;

          (K * |.(x1 - x0).|) <= (K * s) by A5, A18, XREAL_1: 64;

          then

           A21: (K * |.(x1 - x0).|) < r by A17, XXREAL_0: 2;

          

           A23: (F /. x0) = ( integral (f,a,x0)) & (F /. x1) = ( integral (f,a,x1)) by A1, A12, A18;

          reconsider R1 = (F /. x0) as VECTOR of X;

          reconsider R2 = ( integral (f,x0,x1)) as VECTOR of X;

          (((F /. x0) + ( integral (f,x0,x1))) - (F /. x0)) = (((F /. x0) + ( - (F /. x0))) + ( integral (f,x0,x1))) by RLVECT_1:def 3

          .= (( 0. X) + ( integral (f,x0,x1))) by RLVECT_1: 5

          .= ( integral (f,x0,x1));

          then ||.((F /. x1) - (F /. x0)).|| <= (K * |.(x1 - x0).|) by A23, A1, X1, A12, B2, A18, INTEGR21: 29, A20;

          hence thesis by A21, XXREAL_0: 2;

        end;

        hence F is_continuous_in x0 by A1, A12, NFCONT_3: 8;

      end;

    end;

    theorem :: ORDEQ_02:15

    

     Lm00: for f be continuous PartFunc of REAL , the carrier of X st a in ( dom f) holds ( integral (f,a,a)) = ( 0. X)

    proof

      let f be continuous PartFunc of REAL , the carrier of X;

      assume

       A1: a in ( dom f);

       [.a, a.] = {a} by XXREAL_1: 17;

      then

       A2: [.a, a.] c= ( dom f) by A1, ZFMISC_1: 31;

      

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

      then

       A4: ( integral (f, ['a, a'])) = ( integral (f,a,a)) by INTEGR18: 16;

      ( vol ['a, a']) = (a - a) by INTEGRA6: 5;

      hence thesis by A4, A2, A3, INTEGR18: 17;

    end;

    theorem :: ORDEQ_02:16

    

     Th40a: for f be continuous PartFunc of REAL , the carrier of X, g be PartFunc of REAL , the carrier of X st a <= b & ( dom f) = [.a, b.] & for t be Real st t in [.a, b.] holds (g /. t) = (y0 + ( integral (f,a,t))) holds (g /. a) = y0

    proof

      let f be continuous PartFunc of REAL , the carrier of X, g be PartFunc of REAL , the carrier of X;

      assume that

       A1: a <= b and

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

       A6: for t be Real st t in [.a, b.] holds (g /. t) = (y0 + ( integral (f,a,t)));

      

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

      then a in ['a, b'] by A1;

      then ( integral (f,a,a)) = ( 0. X) & (g /. a) = (y0 + ( integral (f,a,a))) by A2, A6, A4, Lm00;

      hence (g /. a) = y0;

    end;

    theorem :: ORDEQ_02:17

    

     Th40: for f be continuous PartFunc of REAL , the carrier of X, g be PartFunc of REAL , the carrier of X st ( dom f) = [.a, b.] & ( dom g) = [.a, b.] & Z = ].a, b.[ & for t be Real st t in [.a, b.] holds (g /. t) = (y0 + ( integral (f,a,t))) holds g is continuous & g is_differentiable_on Z & for t be Real st t in Z holds ( diff (g,t)) = (f /. t)

    proof

      let f be continuous PartFunc of REAL , the carrier of X, g be PartFunc of REAL , the carrier of X;

      assume that

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

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

       D1: Z = ].a, b.[ and

       D2: for t be Real st t in [.a, b.] holds (g /. t) = (y0 + ( integral (f,a,t)));

      deffunc FX( Element of REAL ) = ( integral (f,a,$1));

      consider F0 be Function of REAL , the carrier of X such that

       A5: for x be Element of REAL holds (F0 . x) = FX(x) from FUNCT_2:sch 4;

      set G0 = ( REAL --> y0);

      set F = (F0 | [.a, b.]), G = (G0 | [.a, b.]);

      ( dom F) = (( dom F0) /\ [.a, b.]) & ( dom G) = (( dom G0) /\ [.a, b.]) by RELAT_1: 61;

      then ( dom F) = ( REAL /\ [.a, b.]) & ( dom G) = ( REAL /\ [.a, b.]) by FUNCT_2:def 1;

      then

       A6: ( dom F) = [.a, b.] & ( dom G) = [.a, b.] & ( dom g) = (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 28;

      

       A10: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

      

       A7: for x be Real st x in [.a, b.] holds (F /. x) = ( integral (f,a,x))

      proof

        let x be Real;

        assume x in [.a, b.];

        then

         A8: (F /. x) = (F . x) & (F . x) = (F0 . x) by A6, PARTFUN1:def 6, FUNCT_1: 47;

        x in REAL by XREAL_0:def 1;

        hence (F /. x) = ( integral (f,a,x)) by A5, A8;

      end;

      then

       A12: for x be Real st x in ].a, b.[ holds (F /. x) = ( integral (f,a,x)) by A10;

       A14:

      now

        let x be Real;

        assume

         A15: x in Z;

        then f is_continuous_in x by A10, A2, D1, NFCONT_3:def 2;

        hence F is_differentiable_in x & ( diff (F,x)) = (f /. x) by A15, A2, D1, A12, A10, A6, Th1955;

      end;

      then for x be Real st x in Z holds F is_differentiable_in x;

      then

       A16: F is_differentiable_on Z by D1, A6, XXREAL_1: 25, NDIFF_3: 10;

       A18:

      now

        let x be Real;

        assume

         A19: x in [.a, b.];

        then (G /. x) = (G . x) by A6, PARTFUN1:def 6;

        then (G /. x) = (G0 . x) by A19, A6, FUNCT_1: 47;

        hence (G /. x) = y0 by XREAL_0:def 1, FUNCOP_1: 7;

      end;

      (G | Z) is constant;

      then

       A23: G is_differentiable_on Z & for x be Real st x in Z holds ((G `| Z) . x) = ( 0. X) by A6, D1, A10, NDIFF_3: 20;

      now

        let x be Element of REAL ;

        assume

         A25: x in ( dom g);

        then (G /. x) = y0 & (F /. x) = ( integral (f,a,x)) by A3, A7, A18;

        hence (g /. x) = ((G /. x) + (F /. x)) by A3, D2, A25;

      end;

      then

       A29: g = (G + F) by A6, VFUNCT_1:def 1;

      F is continuous by A6, A7, Th35, A2;

      hence g is continuous by A29;

      thus

       B1: g is_differentiable_on Z by A29, A16, A23, A3, D1, A10, NDIFF_3: 17;

      thus for t be Real st t in Z holds ( diff (g,t)) = (f /. t)

      proof

        let t be Real;

        assume

         A33: t in Z;

        then ( diff (g,t)) = ((g `| Z) . t) & ((g `| Z) . t) = (( diff (G,t)) + ( diff (F,t))) & ( diff (G,t)) = ((G `| Z) . t) & ((G `| Z) . t) = ( 0. X) by A23, B1, A29, A16, NDIFF_3: 17, NDIFF_3:def 6;

        hence ( diff (g,t)) = (f /. t) by A14, A33;

      end;

    end;

    theorem :: ORDEQ_02:18

    

     Th45a: for f be PartFunc of REAL , the carrier of X st a <= b & [.a, b.] c= ( dom f) & (for x be Real st x in [.a, b.] holds f is_continuous_in x) & f is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (f,x)) = ( 0. X) holds (f /. b) = (f /. a)

    proof

      let f be PartFunc of REAL , the carrier of X;

      assume that

       A1: a <= b & [.a, b.] c= ( dom f) & for x be Real st x in [.a, b.] holds f is_continuous_in x and

       A2: f is_differentiable_on ].a, b.[ and

       A3: for x be Real st x in ].a, b.[ holds ( diff (f,x)) = ( 0. X);

      

       A5: for x be Real st x in ].a, b.[ holds f is_differentiable_in x by A2, NDIFF_3: 10;

      now

        let x be Real;

        assume x in ].a, b.[;

        then ||.( diff (f,x)).|| = ||.( 0. X).|| by A3;

        hence ||.( diff (f,x)).|| <= 0 ;

      end;

      then ||.((f /. b) - (f /. a)).|| <= ( 0 * |.(b - a).|) by A5, Th519, A1;

      then ||.((f /. b) - (f /. a)).|| = 0 ;

      hence (f /. b) = (f /. a) by NORMSP_1: 6;

    end;

    theorem :: ORDEQ_02:19

    

     Th45: for f be PartFunc of REAL , the carrier of X st [.a, b.] c= ( dom f) & (for x be Real st x in [.a, b.] holds f is_continuous_in x) & f is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (f,x)) = ( 0. X) holds (f | ].a, b.[) is constant

    proof

      let f be PartFunc of REAL , the carrier of X;

      assume that

       A1: [.a, b.] c= ( dom f) & for x be Real st x in [.a, b.] holds f is_continuous_in x and

       A2: f is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (f,x)) = ( 0. X);

      now

        let x1,x2 be Element of REAL ;

        assume x1 in ( ].a, b.[ /\ ( dom f)) & x2 in ( ].a, b.[ /\ ( dom f));

        then

         A4: x1 in ].a, b.[ & x2 in ].a, b.[ by XBOOLE_0:def 4;

        reconsider Z1 = ].x1, x2.[, Z2 = ].x2, x1.[ as open Subset of REAL ;

        

         A7: ].a, b.[ c= [.a, b.] & Z1 c= [.x1, x2.] & Z2 c= [.x2, x1.] by XXREAL_1: 25;

        then [.x1, x2.] c= [.a, b.] & [.x2, x1.] c= [.a, b.] by A4, XXREAL_2:def 12;

        then

         C1: [.x1, x2.] c= ( dom f) & [.x2, x1.] c= ( dom f) & (for x be Real st x in [.x1, x2.] holds f is_continuous_in x) & (for x be Real st x in [.x2, x1.] holds f is_continuous_in x) by A1;

         [.x1, x2.] c= ].a, b.[ & [.x2, x1.] c= ].a, b.[ by A4, XXREAL_2:def 12;

        then (f is_differentiable_on Z1 & for x be Real st x in Z1 holds ( diff (f,x)) = ( 0. X)) & (f is_differentiable_on Z2 & for x be Real st x in Z2 holds ( diff (f,x)) = ( 0. X)) by A2, A7, NDIFF_3: 24, XBOOLE_1: 1;

        then (x1 < x2 implies (f /. x1) = (f /. x2)) & (x2 < x1 implies (f /. x1) = (f /. x2)) by C1, Th45a;

        hence (f /. x1) = (f /. x2) by XXREAL_0: 1;

      end;

      hence (f | ].a, b.[) is constant by PARTFUN2: 36;

    end;

    theorem :: ORDEQ_02:20

    

     Th46: for f be continuous PartFunc of REAL , the carrier of X st [.a, b.] = ( dom f) & (f | ].a, b.[) is constant holds for x be Real st x in [.a, b.] holds (f /. x) = (f /. a)

    proof

      let f be continuous PartFunc of REAL , the carrier of X;

      assume

       A1: [.a, b.] = ( dom f) & (f | ].a, b.[) is constant;

      

       A2: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

      per cases ;

        suppose

         X0: a >= b;

        hereby

          let x be Real;

          assume x in [.a, b.];

          then a <= x & x <= b by XXREAL_1: 1;

          then a <= x & x <= a by X0, XXREAL_0: 2;

          hence (f /. x) = (f /. a) by XXREAL_0: 1;

        end;

      end;

        suppose

         A0: a < b;

        reconsider d = ((b - a) / 2) as Real;

        

         A3: 0 < (b - a) by A0, XREAL_1: 50;

        then

         A4: 0 < d by XREAL_1: 215;

        (a + ((b - a) / 2)) = ((a + b) / 2);

        then

         A5: a < (a + d) & (a + d) < b by A0, XREAL_1: 226;

        then (a + d) in ].a, b.[;

        then (f . (a + d)) in ( rng f) by A2, A1, FUNCT_1: 3;

        then

        reconsider f0 = (f . (a + d)) as Point of X;

        ( dom (f | ].a, b.[)) = (( dom f) /\ ].a, b.[) by RELAT_1: 61;

        then

         A6: ( dom (f | ].a, b.[)) = ].a, b.[ by A1, XXREAL_1: 25, XBOOLE_1: 28;

         A7:

        now

          let x be Real;

          assume

           A8: x in ].a, b.[;

          

           A9: (a + d) in ( dom (f | ].a, b.[)) by A5, A6;

          

          thus (f /. x) = (f . x) by A8, A2, A1, PARTFUN1:def 6

          .= ((f | ].a, b.[) . x) by A6, A8, FUNCT_1: 47

          .= ((f | ].a, b.[) . (a + d)) by A1, A6, A8, A9, FUNCT_1:def 10

          .= f0 by A9, FUNCT_1: 47;

        end;

        a in ( dom f) & b in ( dom f) by A1, A0;

        then

         A14: f is_continuous_in a & f is_continuous_in b by NFCONT_3:def 2;

        deffunc F1( Nat) = (a + (d / ($1 + 1)));

        

         A12: for x be Element of NAT holds F1(x) is Element of REAL by XREAL_0:def 1;

        consider s1 be Real_Sequence such that

         A13: for x be Element of NAT holds (s1 . x) = F1(x) from FUNCT_2:sch 9( A12);

         A15:

        now

          let y be object;

          assume y in ( rng s1);

          then

          consider x be object such that

           A16: x in ( dom s1) & y = (s1 . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A16;

          

           A17: y = (a + (d / (x + 1))) by A13, A16;

           0 < (d / (x + 1)) by A4, XREAL_1: 139;

          then

           A20: (a + 0 qua Real) < (a + (d / (x + 1))) by XREAL_1: 8;

          (1 + 0 qua Real) <= (1 + x) by XREAL_1: 7;

          then (d / (x + 1)) <= (d / 1) by XREAL_1: 118, A3;

          then (a + (d / (x + 1))) <= (a + d) by XREAL_1: 7;

          then (a + (d / (x + 1))) < b by A5, XXREAL_0: 2;

          hence y in ].a, b.[ by A17, A20;

        end;

        then

         A21: ( rng s1) c= ].a, b.[ & ( rng s1) c= ( dom f) by A2, A1;

         A23:

        now

          let p be Real;

          assume

           A24: 0 < p;

          consider n be Nat such that

           A25: (d / p) < n by SEQ_4: 3;

          (n + 0 qua Real) < (n + 1) by XREAL_1: 8;

          then (d / p) < (n + 1) by XXREAL_0: 2, A25;

          then ((d / p) * p) < ((n + 1) * p) by A24, XREAL_1: 68;

          then d < ((n + 1) * p) by A24, XCMPLX_1: 87;

          then (d / (n + 1)) < p by XREAL_1: 83;

          then

           A29: |.(d / (n + 1)).| < p by A3, ABSVALUE:def 1;

          

           A28: |.(d / (n + 1)).| = (d / (n + 1)) by A3, ABSVALUE:def 1;

          take n;

          thus for m be Nat st n <= m holds |.((s1 . m) - a).| < p

          proof

            let m be Nat;

            

             K: m in NAT by ORDINAL1:def 12;

            assume n <= m;

            then (n + 1) <= (m + 1) by XREAL_1: 7;

            then (d / (m + 1)) <= (d / (n + 1)) by A3, XREAL_1: 118;

            then

             A31: |.(d / (m + 1)).| <= |.(d / (n + 1)).| by A28, A3, ABSVALUE:def 1;

             |.((s1 . m) - a).| = |.((a + (d / (m + 1))) - a).| by A13, K;

            hence |.((s1 . m) - a).| < p by A31, A29, XXREAL_0: 2;

          end;

        end;

        then

         A32: s1 is convergent by SEQ_2:def 6;

        then ( lim s1) = a by A23, SEQ_2:def 7;

        then

         A34: (f /* s1) is convergent & (f /. a) = ( lim (f /* s1)) by A14, A21, A32;

        

         A35: for i be Nat holds ((f /* s1) . i) = f0

        proof

          let i be Nat;

          

           S: i in NAT by ORDINAL1:def 12;

          

           A36: (s1 . i) in ( rng s1) by FUNCT_2: 4, ORDINAL1:def 12;

          

          thus ((f /* s1) . i) = (f /. (s1 . i)) by A21, FUNCT_2: 109, S

          .= f0 by A7, A36, A15;

        end;

        now

          let r be Real;

          assume

           A37: 0 < r;

          reconsider m = the Element of NAT as Nat;

          take m;

          thus for k be Nat st m <= k holds ||.(((f /* s1) . k) - f0).|| < r

          proof

            let k be Nat;

            assume m <= k;

             ||.(((f /* s1) . k) - f0).|| = ||.(f0 - f0).|| by A35

            .= ||.( 0. X).|| by RLVECT_1: 15;

            hence thesis by A37;

          end;

        end;

        then

         A38: (f /. a) = f0 by A34, NORMSP_1:def 7;

        deffunc F2( Nat) = (b - (d / ($1 + 1)));

        

         A39: for x be Element of NAT holds F2(x) is Element of REAL by XREAL_0:def 1;

        consider s2 be Real_Sequence such that

         A40: for x be Element of NAT holds (s2 . x) = F2(x) from FUNCT_2:sch 9( A39);

         A42:

        now

          let y be object;

          assume y in ( rng s2);

          then

          consider x be object such that

           A43: x in ( dom s2) & y = (s2 . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A43;

          

           A44: y = (b - (d / (x + 1))) by A40, A43;

           0 < (d / (x + 1)) by A4, XREAL_1: 139;

          then

           A47: (b - (d / (x + 1))) < (b - 0 qua Real) by XREAL_1: 15;

          (1 + 0 qua Real) <= (1 + x) by XREAL_1: 7;

          then (d / (x + 1)) <= (d / 1) by XREAL_1: 118, A3;

          then (b - d) <= (b - (d / (x + 1))) by XREAL_1: 13;

          then a < (b - (d / (x + 1))) by A5, XXREAL_0: 2;

          hence y in ].a, b.[ by A44, A47;

        end;

        then

         A48: ( rng s2) c= ].a, b.[ & ( rng s2) c= ( dom f) by A2, A1;

         A50:

        now

          let p be Real;

          assume

           A51: 0 < p;

          consider n be Nat such that

           A52: (d / p) < n by SEQ_4: 3;

          (n + 0 qua Real) < (n + 1) by XREAL_1: 8;

          then (d / p) < (n + 1) by XXREAL_0: 2, A52;

          then ((d / p) * p) < ((n + 1) * p) by A51, XREAL_1: 68;

          then d < ((n + 1) * p) by A51, XCMPLX_1: 87;

          then

           A54: (d / (n + 1)) < p by XREAL_1: 83;

          take n;

          thus for m be Nat st n <= m holds |.((s2 . m) - b).| < p

          proof

            let m be Nat;

            

             K: m in NAT by ORDINAL1:def 12;

            assume n <= m;

            then (n + 1) <= (m + 1) by XREAL_1: 7;

            then (d / (m + 1)) <= (d / (n + 1)) by A3, XREAL_1: 118;

            then

             A57: |.(d / (m + 1)).| <= (d / (n + 1)) by A3, ABSVALUE:def 1;

             |.((s2 . m) - b).| = |.((b - (d / (m + 1))) - b).| by A40, K

            .= |.(d / (m + 1)).| by COMPLEX1: 52;

            hence |.((s2 . m) - b).| < p by A57, XXREAL_0: 2, A54;

          end;

        end;

        then

         A58: s2 is convergent by SEQ_2:def 6;

        then ( lim s2) = b by A50, SEQ_2:def 7;

        then

         A60: (f /* s2) is convergent & (f /. b) = ( lim (f /* s2)) by A14, A48, A58;

        

         A61: for i be Element of NAT holds ((f /* s2) . i) = f0

        proof

          let i be Element of NAT ;

          (s2 . i) in ( rng s2) by FUNCT_2: 4;

          then (f /. (s2 . i)) = f0 by A7, A42;

          hence ((f /* s2) . i) = f0 by A48, FUNCT_2: 109;

        end;

        now

          let r be Real;

          assume

           A63: 0 < r;

          reconsider m = the Element of NAT as Nat;

          take m;

          thus for k be Nat st m <= k holds ||.(((f /* s2) . k) - f0).|| < r

          proof

            let k be Nat;

            assume m <= k;

            k in NAT by ORDINAL1:def 12;

            

            then ||.(((f /* s2) . k) - f0).|| = ||.(f0 - f0).|| by A61

            .= ||.( 0. X).|| by RLVECT_1: 15

            .= 0 ;

            hence thesis by A63;

          end;

        end;

        then

         A64: (f /. b) = f0 by A60, NORMSP_1:def 7;

        let x be Real;

        assume x in [.a, b.];

        then

         A65: ex r be Real st x = r & a <= r & r <= b;

        per cases ;

          suppose x in ].a, b.[;

          hence (f /. x) = (f /. a) by A38, A7;

        end;

          suppose not x in ].a, b.[;

          then x <= a or b <= x;

          hence (f /. x) = (f /. a) by A38, A64, A65, XXREAL_0: 1;

        end;

      end;

    end;

    theorem :: ORDEQ_02:21

    

     Th47: for y,Gf be continuous PartFunc of REAL , the carrier of X, g be PartFunc of REAL , the carrier of X st a <= b & Z = ].a, b.[ & ( dom y) = [.a, b.] & ( dom g) = [.a, b.] & ( dom Gf) = [.a, b.] & y is_differentiable_on Z & (y /. a) = y0 & (for t be Real st t in Z holds ( diff (y,t)) = (Gf /. t)) & (for t be Real st t in [.a, b.] holds (g /. t) = (y0 + ( integral (Gf,a,t)))) holds y = g

    proof

      let y,Gf be continuous PartFunc of REAL , the carrier of X, g be PartFunc of REAL , the carrier of X;

      assume

       A1: a <= b & Z = ].a, b.[ & ( dom y) = [.a, b.] & ( dom g) = [.a, b.] & ( dom Gf) = [.a, b.] & y is_differentiable_on Z & (y /. a) = y0 & (for t be Real st t in Z holds ( diff (y,t)) = (Gf /. t)) & (for t be Real st t in [.a, b.] holds (g /. t) = (y0 + ( integral (Gf,a,t))));

      then

       A2: g is continuous & (g /. a) = y0 & g is_differentiable_on Z & for t be Real st t in Z holds ( diff (g,t)) = (Gf /. t) by Th40, Th40a;

      reconsider h = (y - g) as continuous PartFunc of REAL , the carrier of X by A2;

      

       A5: ( dom h) = ( [.a, b.] /\ [.a, b.]) by A1, VFUNCT_1:def 2;

      then

       A7: h is_differentiable_on ].a, b.[ by A1, A2, NDIFF_3: 18;

       A8:

      now

        let x be Real;

        assume

         A9: x in ].a, b.[;

        then

         A10: ( diff (y,x)) = (Gf /. x) & ( diff (g,x)) = (Gf /. x) by A1, Th40;

        

        thus ( diff (h,x)) = (((y - g) `| ].a, b.[) . x) by A9, A7, NDIFF_3:def 6

        .= ((Gf /. x) - (Gf /. x)) by A10, A1, A2, A5, A9, NDIFF_3: 18

        .= ( 0. X) by RLVECT_1: 15;

      end;

      for x be Real st x in [.a, b.] holds h is_continuous_in x by A5, NFCONT_3:def 2;

      then

       A12: (h | ].a, b.[) is constant by A1, Th45, A5, A2, NDIFF_3: 18, A8;

      

       A13: for x be Real st x in ( dom h) holds (h /. x) = ( 0. X)

      proof

        let x be Real;

        assume

         A14: x in ( dom h);

        

         A15: a in ( dom h) by A5, A1;

        

        thus (h /. x) = (h /. a) by A14, Th46, A12, A5

        .= (y0 - y0) by A2, A1, A15, VFUNCT_1:def 2

        .= ( 0. X) by RLVECT_1: 15;

      end;

      for x be Element of REAL st x in ( dom y) holds (y . x) = (g . x)

      proof

        let x be Element of REAL ;

        assume

         A16: x in ( dom y);

        

        then ( 0. X) = (h /. x) by A13, A1, A5

        .= ((y /. x) - (g /. x)) by A16, A1, A5, VFUNCT_1:def 2;

        then

         A17: (y /. x) = (g /. x) by RLVECT_1: 21;

        

        thus (y . x) = (y /. x) by A16, PARTFUN1:def 6

        .= (g . x) by A17, A16, A1, PARTFUN1:def 6;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    

     Lm4: for n be Nat holds for a,r,L be Real, g be Function of REAL , REAL st for x be Real holds (g . x) = ((((r * (x - a)) |^ (n + 1)) / ((n + 1) ! )) * L) holds for x be Real holds g is_differentiable_in x & ( diff (g,x)) = (r * ((((r * (x - a)) |^ n) / (n ! )) * L))

    proof

      let n be Nat, a,r,L be Real, g be Function of REAL , REAL ;

      assume

       A1: for x be Real holds (g . x) = ((((r * (x - a)) |^ (n + 1)) / ((n + 1) ! )) * L);

      

       A2: ( dom g) = REAL by FUNCT_2:def 1;

      deffunc F( Real) = ( In (((($1 - a) |^ (n + 1)) / ((n + 1) ! )), REAL ));

      consider f be Function of REAL , REAL such that

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

      

       a3: for x be Real holds (f . x) = (((x - a) |^ (n + 1)) / ((n + 1) ! ))

      proof

        let x be Real;

        x in REAL by XREAL_0:def 1;

        then (f . x) = F(x) by A3;

        hence thesis;

      end;

      

       A5: ( dom (((r |^ (n + 1)) * L) (#) f)) = REAL by FUNCT_2:def 1;

      now

        let x be Element of REAL ;

        assume x in ( dom (((r |^ (n + 1)) * L) (#) f));

        

        hence ((((r |^ (n + 1)) * L) (#) f) . x) = (((r |^ (n + 1)) * L) * (f . x)) by VALUED_1:def 5

        .= (((r |^ (n + 1)) * L) * (((x - a) |^ (n + 1)) / ((n + 1) ! ))) by a3

        .= ((((r |^ (n + 1)) * ((x - a) |^ (n + 1))) / ((n + 1) ! )) * L)

        .= ((((r * (x - a)) |^ (n + 1)) / ((n + 1) ! )) * L) by NEWTON: 7

        .= (g . x) by A1;

      end;

      then

       A6: (((r |^ (n + 1)) * L) (#) f) = g by PARTFUN1: 5, A2, A5;

      for x be Real holds (((r |^ (n + 1)) * L) (#) f) is_differentiable_in x & ( diff ((((r |^ (n + 1)) * L) (#) f),x)) = (r * ((((r * (x - a)) |^ n) / (n ! )) * L))

      proof

        let x be Real;

        

         A8: f is_differentiable_in x & ( diff (f,x)) = (((x - a) |^ n) / (n ! )) by ORDEQ_01: 47, a3;

        hence (((r |^ (n + 1)) * L) (#) f) is_differentiable_in x by FDIFF_1: 15;

        

        thus ( diff ((((r |^ (n + 1)) * L) (#) f),x)) = (((r |^ (n + 1)) * L) * ( diff (f,x))) by A8, FDIFF_1: 15

        .= ((((r |^ (n + 1)) * ((x - a) |^ n)) / (n ! )) * L) by A8

        .= ((((r * (r |^ n)) * ((x - a) |^ n)) / (n ! )) * L) by NEWTON: 6

        .= (((r * ((r |^ n) * ((x - a) |^ n))) / (n ! )) * L)

        .= (((r * ((r * (x - a)) |^ n)) / (n ! )) * L) by NEWTON: 7

        .= (r * ((((r * (x - a)) |^ n) / (n ! )) * L));

      end;

      hence thesis by A6;

    end;

    

     Lm5: for m be non zero Element of NAT , a,r,L be Real, g be Function of REAL , REAL st (for x be Real holds (g . x) = (r * ((((r * (x - a)) |^ m) / (m ! )) * L))) holds for x be Real holds g is_differentiable_in x

    proof

      let m be non zero Element of NAT , a,r,L be Real, g be Function of REAL , REAL ;

      assume

       A1: for x be Real holds (g . x) = (r * ((((r * (x - a)) |^ m) / (m ! )) * L));

      

       A2: ( dom g) = REAL by FUNCT_2:def 1;

      reconsider n = (m - 1) as Element of NAT by ORDINAL1:def 12;

      deffunc F( Real) = ( In (((($1 - a) |^ (n + 1)) / ((n + 1) ! )), REAL ));

      consider f be Function of REAL , REAL such that

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

      

       a3: for x be Real holds (f . x) = (((x - a) |^ (n + 1)) / ((n + 1) ! ))

      proof

        let x be Real;

        x in REAL by XREAL_0:def 1;

        then (f . x) = F(x) by A3;

        hence thesis;

      end;

      

       A5: ( dom (((r |^ (n + 2)) * L) (#) f)) = REAL by FUNCT_2:def 1;

       A6:

      now

        let x be Element of REAL ;

        assume x in ( dom (((r |^ (n + 2)) * L) (#) f));

        

        hence ((((r |^ (n + 2)) * L) (#) f) . x) = (((r |^ (n + 2)) * L) * (f . x)) by VALUED_1:def 5

        .= (((r |^ (n + 2)) * L) * (((x - a) |^ (n + 1)) / ((n + 1) ! ))) by a3

        .= (((r |^ ((n + 1) + 1)) * (((x - a) |^ (n + 1)) / ((n + 1) ! ))) * L)

        .= (((r * (r |^ (n + 1))) * (((x - a) |^ (n + 1)) / ((n + 1) ! ))) * L) by NEWTON: 6

        .= ((r * (((r |^ (n + 1)) * ((x - a) |^ (n + 1))) / ((n + 1) ! ))) * L)

        .= ((r * (((r * (x - a)) |^ (n + 1)) / ((n + 1) ! ))) * L) by NEWTON: 7

        .= (r * ((((r * (x - a)) |^ m) / (m ! )) * L))

        .= (g . x) by A1;

      end;

      

       A7: for x be Real holds (((r |^ (n + 2)) * L) (#) f) is_differentiable_in x

      proof

        let x be Real;

        f is_differentiable_in x by ORDEQ_01: 47, a3;

        hence (((r |^ (n + 2)) * L) (#) f) is_differentiable_in x by FDIFF_1: 15;

      end;

      (((r |^ (n + 2)) * L) (#) f) = g by A6, A2, A5, PARTFUN1: 5;

      hence thesis by A7;

    end;

    

     Lm6: for n be non zero Element of NAT , a,r,t,L be Real, f0 be Function of REAL , REAL st a <= t & for x be Real holds (f0 . x) = (r * ((((r * (x - a)) |^ n) / (n ! )) * L)) holds (f0 | [.a, t.]) is continuous & (f0 | [.a, t.]) is bounded & f0 is_integrable_on ['a, t'] & ( integral (f0,a,t)) = ((((r * (t - a)) |^ (n + 1)) / ((n + 1) ! )) * L)

    proof

      let n be non zero Element of NAT ;

      let a,r,t,L be Real, f0 be Function of REAL , REAL ;

      

       S: a in REAL by XREAL_0:def 1;

      assume

       A1: a <= t;

      assume

       A2: for x be Real holds (f0 . x) = (r * ((((r * (x - a)) |^ n) / (n ! )) * L));

      

       A5: ( dom f0) = REAL by FUNCT_2:def 1;

      for x be Real st x in ( dom f0) holds f0 is_continuous_in x by A2, Lm5, FDIFF_1: 24;

      then

      reconsider f0 as continuous PartFunc of REAL , REAL by FCONT_1:def 2;

      deffunc F( Real) = ( In (((((r * ($1 - a)) |^ (n + 1)) / ((n + 1) ! )) * L), REAL ));

      consider g be Function of REAL , REAL such that

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

      

       a6: for x be Real holds (g . x) = ((((r * (x - a)) |^ (n + 1)) / ((n + 1) ! )) * L)

      proof

        let x be Real;

        x in REAL by XREAL_0:def 1;

        then (g . x) = ( In (((((r * (x - a)) |^ (n + 1)) / ((n + 1) ! )) * L), REAL )) by A6;

        hence thesis;

      end;

      then

       A8: g is_differentiable_on REAL by Lm4, FUNCT_2:def 1;

       A9:

      now

        let x be Element of REAL ;

        assume x in ( dom (g `| ( [#] REAL )));

        

        thus ((g `| ( [#] REAL )) . x) = ( diff (g,x)) by A8, FDIFF_1:def 7

        .= (r * ((((r * (x - a)) |^ n) / (n ! )) * L)) by Lm4, a6

        .= ((f0 | ( [#] REAL )) . x) by A2;

      end;

      ( dom (g `| ( [#] REAL ))) = ( [#] REAL ) by A8, FDIFF_1:def 7

      .= ( dom (f0 | ( [#] REAL ))) by FUNCT_2:def 1;

      then (g `| ( [#] REAL )) = (f0 | ( [#] REAL )) by A9, PARTFUN1: 5;

      then g in ( IntegralFuncs (f0,( [#] REAL ))) by A8, INTEGRA7:def 1;

      then

       A10: g is_integral_of (f0,( [#] REAL )) by INTEGRA7:def 2;

      

       A11: (f0 | ['a, t']) is bounded by INTEGRA5: 10, A5;

      

       A12: (g . t) = (( integral (f0,a,t)) + (g . a)) by A1, INTEGRA7: 18, A5, INTEGRA5: 11, A11, A10;

      

       A13: ( 0 qua Real + 1) <= (n + 1) by XREAL_1: 6;

      (g . a) = ( In (((((r * (a - a)) |^ (n + 1)) / ((n + 1) ! )) * L), REAL )) by A6, S

      .= (( 0 qua Real / ((n + 1) ! )) * L) by A13, NEWTON: 11

      .= 0 qua Real;

      hence thesis by A11, A12, A5, INTEGRA5: 11, a6, A1, INTEGRA5:def 3;

    end;

    

     Lm7: for a,t,L,r be Real, k be non zero Element of NAT st a <= t holds ex rg be PartFunc of REAL , REAL st ( dom rg) = [.a, t.] & (for x be Real st x in [.a, t.] holds (rg . x) = (r * ((((r * (x - a)) |^ k) / (k ! )) * L))) & rg is continuous & rg is_integrable_on ['a, t'] & (rg | [.a, t.]) is bounded & ( integral (rg,a,t)) = ((((r * (t - a)) |^ (k + 1)) / ((k + 1) ! )) * L)

    proof

      let a,t,L,r be Real, k be non zero Element of NAT ;

      assume

       A1: a <= t;

      then

       X1: ['a, t'] = [.a, t.] by INTEGRA5:def 3;

      deffunc F( Real) = ( In ((r * ((((r * ($1 - a)) |^ k) / (k ! )) * L)), REAL ));

      consider f0 be Function of REAL , REAL such that

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

      

       a2: for x be Real holds (f0 . x) = (r * ((((r * (x - a)) |^ k) / (k ! )) * L))

      proof

        let x be Real;

        x in REAL by XREAL_0:def 1;

        then (f0 . x) = ( In ((r * ((((r * (x - a)) |^ k) / (k ! )) * L)), REAL )) by A2;

        hence thesis;

      end;

      

       A3: ( dom f0) = REAL by FUNCT_2:def 1;

      

       A4: (f0 | [.a, t.]) is continuous & (f0 | [.a, t.]) is bounded & f0 is_integrable_on ['a, t'] & ( integral (f0,a,t)) = ((((r * (t - a)) |^ (k + 1)) / ((k + 1) ! )) * L) by Lm6, A1, a2;

      set f = (f0 | [.a, t.]);

      reconsider f as continuous PartFunc of REAL , REAL by Lm6, A1, a2;

       A7:

      now

        let x be Real;

        assume

         A8: x in [.a, t.];

        

         A9: x in REAL by XREAL_0:def 1;

        

        thus (f . x) = (f0 . x) by A8, FUNCT_1: 49

        .= ( In ((r * ((((r * (x - a)) |^ k) / (k ! )) * L)), REAL )) by A2, A9

        .= (r * ((((r * (x - a)) |^ k) / (k ! )) * L));

      end;

      

       A10: ( integral (f0,a,t)) = ( integral (f0, ['a, t'])) & ( integral (f,a,t)) = ( integral (f, ['a, t'])) by INTEGRA5:def 4, A1;

      take f;

      thus thesis by A7, A10, A4, A3, X1, RELAT_1: 62;

    end;

    definition

      let X be RealBanachSpace;

      let y0 be VECTOR of X, G be Function of X, X, a,b be Real;

      assume

       A1: a <= b & G is_continuous_on ( dom G);

      :: ORDEQ_02:def1

      func Fredholm (G,a,b,y0) -> Function of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)), ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) means

      : Def8: for x be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) holds ex f,g,Gf be continuous PartFunc of REAL , the carrier of X st x = f & (it . x) = g & ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Gf = (G * f) & for t be Real st t in ['a, b'] holds (g /. t) = (y0 + ( integral (Gf,a,t)));

      existence

      proof

        defpred P[ set, set] means ex f,g,Gf be continuous PartFunc of REAL , the carrier of X st $1 = f & $2 = g & ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Gf = (G * f) & for t be Real st t in ['a, b'] holds (g /. t) = (y0 + ( integral (Gf,a,t)));

        set D = the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

        

         X1: the carrier of X = ( dom G) by FUNCT_2:def 1;

        

         A2: for x be Element of D holds ex y be Element of D st P[x, y]

        proof

          let x be Element of D;

          consider f0 be continuous PartFunc of REAL , the carrier of X such that

           A3: x = f0 & ( dom f0) = ['a, b'] by ORDEQ_01:def 2;

          now

            let x0 be Real;

            assume

             A4: x0 in ( dom (G * f0));

            then f0 is_continuous_in x0 by NFCONT_3:def 2, FUNCT_1: 11;

            hence (G * f0) is_continuous_in x0 by A4, X1, NFCONT_3: 15, A1;

          end;

          then

          reconsider Gf = (G * f0) as continuous PartFunc of REAL , the carrier of X by NFCONT_3:def 2;

          ( rng f0) c= ( dom G) by X1;

          then

           A6: ( dom Gf) = ['a, b'] by A3, RELAT_1: 27;

          

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

          deffunc FX( Element of REAL ) = ( integral (Gf,a,$1));

          consider F0 be Function of REAL , the carrier of X such that

           A8: for x be Element of REAL holds (F0 . x) = FX(x) from FUNCT_2:sch 4;

          set F = (F0 | ['a, b']);

          ( dom F0) = REAL by FUNCT_2:def 1;

          then

           A9: ( dom F) = ['a, b'] by RELAT_1: 62;

           A10:

          now

            let t be Real;

            assume

             A11: t in [.a, b.];

            

             A12: t in REAL by XREAL_0:def 1;

            

            thus (F /. t) = (F . t) by A7, A9, A11, PARTFUN1:def 6

            .= (F0 . t) by A11, A9, A7, FUNCT_1: 47

            .= ( integral (Gf,a,t)) by A8, A12;

          end;

          set G0 = ( REAL --> y0);

          set G1 = (G0 | ['a, b']);

          ( dom G0) = REAL ;

          then

           A14: ( dom G1) = ['a, b'] by RELAT_1: 62;

           A15:

          now

            let t be Real;

            assume

             A16: t in [.a, b.];

            

            hence (G1 /. t) = (G1 . t) by A7, A14, PARTFUN1:def 6

            .= (G0 . t) by A16, A14, A7, FUNCT_1: 47

            .= y0 by XREAL_0:def 1, FUNCOP_1: 7;

          end;

          set g = (G1 + F);

          

           A19: ( dom g) = (( dom F) /\ ( dom G1)) by VFUNCT_1:def 1

          .= ['a, b'] by A9, A14;

          F is continuous by A7, A9, Th35, A6, A10;

          then

          reconsider g as continuous PartFunc of REAL , the carrier of X;

          reconsider y = g as Element of D by A19, ORDEQ_01:def 2;

          take y;

          now

            let t be Real;

            assume

             A20: t in ['a, b'];

            then (G1 /. t) = y0 & (F /. t) = ( integral (Gf,a,t)) by A7, A10, A15;

            hence (g /. t) = (y0 + ( integral (Gf,a,t))) by A19, A20, VFUNCT_1:def 1;

          end;

          hence thesis by A19, A3;

        end;

        consider F be Function of D, D such that

         A23: for x be Element of D holds P[x, (F . x)] from FUNCT_2:sch 3( A2);

        take F;

        thus thesis by A23;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)), ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

        assume

         A24: for x be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) holds ex f,g,Gf be continuous PartFunc of REAL , the carrier of X st x = f & (F1 . x) = g & ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Gf = (G * f) & for t be Real st t in ['a, b'] holds (g /. t) = (y0 + ( integral (Gf,a,t)));

        assume

         A25: for x be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) holds ex f,g,Gf be continuous PartFunc of REAL , the carrier of X st x = f & (F2 . x) = g & ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Gf = (G * f) & for t be Real st t in ['a, b'] holds (g /. t) = (y0 + ( integral (Gf,a,t)));

        now

          let x be Element of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

          consider f1,g1,Gf1 be continuous PartFunc of REAL , the carrier of X such that

           A26: x = f1 & (F1 . x) = g1 & ( dom f1) = ['a, b'] & ( dom g1) = ['a, b'] & Gf1 = (G * f1) & for t be Real st t in ['a, b'] holds (g1 /. t) = (y0 + ( integral (Gf1,a,t))) by A24;

          consider f2,g2,Gf2 be continuous PartFunc of REAL , the carrier of X such that

           A27: x = f2 & (F2 . x) = g2 & ( dom f2) = ['a, b'] & ( dom g2) = ['a, b'] & Gf2 = (G * f2) & for t be Real st t in ['a, b'] holds (g2 /. t) = (y0 + ( integral (Gf2,a,t))) by A25;

          now

            let t be object;

            assume

             A28: t in ( dom g1);

            then

            reconsider t0 = t as Real;

            

             A29: (g1 /. t) = (y0 + ( integral (Gf2,a,t0))) by A27, A28, A26

            .= (g2 /. t) by A28, A27, A26;

            

            thus (g1 . t) = (g1 /. t) by A28, PARTFUN1:def 6

            .= (g2 . t) by A26, A27, A28, A29, PARTFUN1:def 6;

          end;

          hence (F1 . x) = (F2 . x) by A26, A27, FUNCT_1: 2;

        end;

        hence F1 = F2 by FUNCT_2:def 8;

      end;

    end

    theorem :: ORDEQ_02:22

    

     Th53: a <= b & 0 < r & (for y1,y2 be VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||)) implies for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)), g,h be continuous PartFunc of REAL , the carrier of X st g = (( Fredholm (G,a,b,y0)) . u) & h = (( Fredholm (G,a,b,y0)) . v) holds for t be Real st t in ['a, b'] holds ||.((g /. t) - (h /. t)).|| <= ((r * (t - a)) * ||.(u - v).||)

    proof

      assume

       A1: a <= b & 0 < r & for y1,y2 be VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||);

      

       A2: ( dom G) = the carrier of X by FUNCT_2:def 1;

      for x1,x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds ||.((G /. x1) - (G /. x2)).|| <= (r * ||.(x1 - x2).||) by A1;

      then G is_Lipschitzian_on the carrier of X by A1, FUNCT_2:def 1;

      then

       A3: G is_continuous_on ( dom G) by A2, NFCONT_1: 45;

      let u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)), g,h be continuous PartFunc of REAL , the carrier of X;

      assume

       A4: g = (( Fredholm (G,a,b,y0)) . u) & h = (( Fredholm (G,a,b,y0)) . v);

      set F = ( Fredholm (G,a,b,y0));

      consider f1,g1,Gf1 be continuous PartFunc of REAL , the carrier of X such that

       A5: u = f1 & (F . u) = g1 & ( dom f1) = ['a, b'] & ( dom g1) = ['a, b'] & Gf1 = (G * f1) & for t be Real st t in ['a, b'] holds (g1 /. t) = (y0 + ( integral (Gf1,a,t))) by Def8, A1, A3;

      consider f2,g2,Gf2 be continuous PartFunc of REAL , the carrier of X such that

       A6: v = f2 & (F . v) = g2 & ( dom f2) = ['a, b'] & ( dom g2) = ['a, b'] & Gf2 = (G * f2) & for t be Real st t in ['a, b'] holds (g2 /. t) = (y0 + ( integral (Gf2,a,t))) by Def8, A1, A3;

      set Gf12 = (Gf1 - Gf2);

      ( dom G) = the carrier of X by FUNCT_2:def 1;

      then ( rng f1) c= ( dom G) & ( rng f2) c= ( dom G);

      then

       A8: ( dom Gf1) = ['a, b'] & ( dom Gf2) = ['a, b'] by A5, A6, RELAT_1: 27;

      reconsider Gf12 as continuous PartFunc of REAL , the carrier of X;

      

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

      then

       A18: a in ['a, b'] by A1;

      let t be Real;

      assume

       A11: t in ['a, b'];

      then

       A12: ex g be Real st t = g & a <= g & g <= b by A10;

      then

       A20: ['a, t'] c= ['a, b'] by INTEGR19: 1;

      

       X1: ['a, t'] = [.a, t.] by A12, INTEGRA5:def 3;

      

       A13: ( dom Gf12) = (( dom Gf1) /\ ( dom Gf2)) by VFUNCT_1:def 2;

      for x be Real st x in ['a, t'] holds ||.(Gf12 /. x).|| <= (r * ||.(u - v).||)

      proof

        let x be Real;

        assume

         A19: x in ['a, t'];

        then

         A21: (Gf12 /. x) = ((Gf1 /. x) - (Gf2 /. x)) by A8, A13, A20, VFUNCT_1:def 2;

        

         A24: (r * ||.((f1 /. x) - (f2 /. x)).||) <= (r * ||.(u - v).||) by A1, XREAL_1: 64, A19, A20, A5, A6, ORDEQ_01: 26;

        

         A22: (Gf1 /. x) = (Gf1 . x) by A8, A20, A19, PARTFUN1:def 6

        .= (G . (f1 . x)) by A20, A19, A8, A5, FUNCT_1: 12

        .= (G /. (f1 /. x)) by A20, A19, A5, PARTFUN1:def 6;

        (Gf2 /. x) = (Gf2 . x) by A8, A20, A19, PARTFUN1:def 6

        .= (G . (f2 . x)) by A20, A19, A8, A6, FUNCT_1: 12

        .= (G /. (f2 /. x)) by A20, A19, A6, PARTFUN1:def 6;

        then ||.((Gf1 /. x) - (Gf2 /. x)).|| <= (r * ||.((f1 /. x) - (f2 /. x)).||) by A22, A1;

        hence thesis by A21, A24, XXREAL_0: 2;

      end;

      then

       A25: ||.( integral (Gf12,a,t)).|| <= ((r * ||.(u - v).||) * (t - a)) by Lm14a, X1, A8, A13, A18, A10, A11, A12;

      (g /. t) = (y0 + ( integral (Gf1,a,t))) & (h /. t) = (y0 + ( integral (Gf2,a,t))) by A4, A5, A6, A11;

      

      then ((g /. t) - (h /. t)) = (((y0 + ( integral (Gf1,a,t))) - y0) - ( integral (Gf2,a,t))) by RLVECT_1: 27

      .= ((( integral (Gf1,a,t)) + (y0 - y0)) - ( integral (Gf2,a,t))) by RLVECT_1: 28

      .= ((( integral (Gf1,a,t)) + ( 0. X)) - ( integral (Gf2,a,t))) by RLVECT_1: 15

      .= ( integral (Gf12,a,t)) by A8, A18, A11, A1, INTEGR21: 30;

      hence thesis by A25;

    end;

    theorem :: ORDEQ_02:23

    

     Th54: a <= b & 0 < r & (for y1,y2 be VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||)) implies for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)), m be Element of NAT , g,h be continuous PartFunc of REAL , the carrier of X st g = (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . u) & h = (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . v) holds for t be Real st t in ['a, b'] holds ||.((g /. t) - (h /. t)).|| <= ((((r * (t - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||)

    proof

      assume

       A1: a <= b & 0 < r & for y1,y2 be VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||);

      set F = ( Fredholm (G,a,b,y0));

      

       A2: ( dom G) = the carrier of X by FUNCT_2:def 1;

      for x1,x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds ||.((G /. x1) - (G /. x2)).|| <= (r * ||.(x1 - x2).||) by A1;

      then G is_Lipschitzian_on the carrier of X by A1, FUNCT_2:def 1;

      then

       A3: G is_continuous_on ( dom G) by A2, NFCONT_1: 45;

      let u1,v1 be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

      defpred P[ Nat] means for g,h be continuous PartFunc of REAL , the carrier of X st g = (( iter (F,($1 + 1))) . u1) & h = (( iter (F,($1 + 1))) . v1) holds for t be Real st t in ['a, b'] holds ||.((g /. t) - (h /. t)).|| <= ((((r * (t - a)) |^ ($1 + 1)) / (($1 + 1) ! )) * ||.(u1 - v1).||);

      reconsider Z0 = 0 as Element of NAT ;

      

       A4: P[ 0 ]

      proof

        let g,h be continuous PartFunc of REAL , the carrier of X;

        assume g = (( iter (F,( 0 qua Element of NAT + 1))) . u1) & h = (( iter (F,( 0 qua Element of NAT + 1))) . v1);

        then

         A6: g = (F . u1) & h = (F . v1) by FUNCT_7: 70;

        for t be Real st t in ['a, b'] holds ||.((g /. t) - (h /. t)).|| <= ((((r * (t - a)) |^ (Z0 + 1)) / ((Z0 + 1) ! )) * ||.(u1 - v1).||) by NEWTON: 13, Th53, A1, A6;

        hence thesis;

      end;

      

       A8: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A9: P[k];

        let g,h be continuous PartFunc of REAL , the carrier of X;

        assume

         A10: g = (( iter (F,((k + 1) + 1))) . u1) & h = (( iter (F,((k + 1) + 1))) . v1);

        reconsider u = (( iter (F,(k + 1))) . u1), v = (( iter (F,(k + 1))) . v1) as VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

        

         A11: ( dom ( iter (F,(k + 1)))) = the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) by FUNCT_2:def 1;

        

         A12: (( iter (F,((k + 1) + 1))) . u1) = ((F * ( iter (F,(k + 1)))) . u1) by FUNCT_7: 71

        .= (F . u) by A11, FUNCT_1: 13;

        

         A13: (( iter (F,((k + 1) + 1))) . v1) = ((F * ( iter (F,(k + 1)))) . v1) by FUNCT_7: 71

        .= (F . v) by A11, FUNCT_1: 13;

        consider f1,g1,Gf1 be continuous PartFunc of REAL , the carrier of X such that

         A14: u = f1 & (F . u) = g1 & ( dom f1) = ['a, b'] & ( dom g1) = ['a, b'] & Gf1 = (G * f1) & for t be Real st t in ['a, b'] holds (g1 /. t) = (y0 + ( integral (Gf1,a,t))) by Def8, A1, A3;

        consider f2,g2,Gf2 be continuous PartFunc of REAL , the carrier of X such that

         A15: v = f2 & (F . v) = g2 & ( dom f2) = ['a, b'] & ( dom g2) = ['a, b'] & Gf2 = (G * f2) & for t be Real st t in ['a, b'] holds (g2 /. t) = (y0 + ( integral (Gf2,a,t))) by Def8, A1, A3;

        set Gf12 = (Gf1 - Gf2);

        ( dom G) = the carrier of X by FUNCT_2:def 1;

        then ( rng f1) c= ( dom G) & ( rng f2) c= ( dom G);

        then

         A18: ( dom Gf1) = ['a, b'] & ( dom Gf2) = ['a, b'] by A14, A15, RELAT_1: 27;

        reconsider Gf12 as continuous PartFunc of REAL , the carrier of X;

        

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

        let t be Real;

        assume

         A21: t in ['a, b'];

        then

         A22: ex g be Real st t = g & a <= g & g <= b by A20;

        

         a22: ex g be Element of REAL st t = g & a <= g & g <= b

        proof

          consider g be Real such that

           H1: t = g & a <= g & g <= b by A21, A20;

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

          take g;

          thus thesis by H1;

        end;

        

         A23: ( dom Gf12) = (( dom Gf1) /\ ( dom Gf2)) by VFUNCT_1:def 2

        .= ['a, b'] by A18;

        then

         A24: ( dom ||.Gf12.||) = ['a, b'] by NORMSP_0:def 2;

        

         A27: a in ['a, b'] by A20, A1;

        ( min (a,t)) = a & ( max (a,t)) = t by A22, XXREAL_0:def 9, XXREAL_0:def 10;

        then

         A30: ||.Gf12.|| is_integrable_on ['a, t'] & ( ||.Gf12.|| | ['a, t']) is bounded & ||.( integral (Gf12,a,t)).|| <= ( integral ( ||.Gf12.||,a,t)) by A1, A23, A27, A21, INTEGR21: 22;

         ['a, t'] = [.a, t.] by A22, INTEGRA5:def 3;

        then

        consider rg be PartFunc of REAL , REAL such that

         A31: ( dom rg) = ['a, t'] & (for x be Real st x in ['a, t'] holds (rg . x) = (r * ((((r * (x - a)) |^ (k + 1)) / ((k + 1) ! )) * ||.(u1 - v1).||))) & rg is continuous & rg is_integrable_on ['a, t'] & (rg | ['a, t']) is bounded & ( integral (rg,a,t)) = ((((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) ! )) * ||.(u1 - v1).||) by Lm7, a22;

        

         A32: ['a, t'] c= ['a, b'] by A22, INTEGR19: 1;

        for x be Real st x in ['a, t'] holds ( ||.Gf12.|| . x) <= (rg . x)

        proof

          let x be Real;

          assume

           A33: x in ['a, t'];

          then

           A34: (Gf12 /. x) = ((Gf1 /. x) - (Gf2 /. x)) by A23, A32, VFUNCT_1:def 2;

          

           A35: (Gf1 /. x) = (Gf1 . x) by A18, A32, A33, PARTFUN1:def 6

          .= (G . (f1 . x)) by A32, A33, A18, A14, FUNCT_1: 12

          .= (G /. (f1 /. x)) by A32, A33, A14, PARTFUN1:def 6;

          (Gf2 /. x) = (Gf2 . x) by A18, A32, A33, PARTFUN1:def 6

          .= (G . (f2 . x)) by A32, A33, A18, A15, FUNCT_1: 12

          .= (G /. (f2 /. x)) by A32, A33, A15, PARTFUN1:def 6;

          then

           A37: ||.((Gf1 /. x) - (Gf2 /. x)).|| <= (r * ||.((f1 /. x) - (f2 /. x)).||) by A35, A1;

          (r * ||.((f1 /. x) - (f2 /. x)).||) <= (r * ((((r * (x - a)) |^ (k + 1)) / ((k + 1) ! )) * ||.(u1 - v1).||)) by A1, XREAL_1: 64, A9, A14, A15, A32, A33;

          then (r * ||.((f1 /. x) - (f2 /. x)).||) <= (rg . x) by A33, A31;

          then ||.((Gf1 /. x) - (Gf2 /. x)).|| <= (rg . x) by A37, XXREAL_0: 2;

          hence thesis by A24, A32, A33, NORMSP_0:def 2, A34;

        end;

        then

         A38: ( integral ( ||.Gf12.||,a,t)) <= ( integral (rg,a,t)) by A30, A22, A24, A32, A31, ORDEQ_01: 48;

        (g /. t) = (y0 + ( integral (Gf1,a,t))) & (h /. t) = (y0 + ( integral (Gf2,a,t))) by A14, A15, A21, A12, A10, A13;

        

        then ((g /. t) - (h /. t)) = (((y0 + ( integral (Gf1,a,t))) - y0) - ( integral (Gf2,a,t))) by RLVECT_1: 27

        .= ((( integral (Gf1,a,t)) + (y0 - y0)) - ( integral (Gf2,a,t))) by RLVECT_1: 28

        .= ((( integral (Gf1,a,t)) + ( 0. X)) - ( integral (Gf2,a,t))) by RLVECT_1: 15

        .= ( integral (Gf12,a,t)) by A18, A27, A21, A1, INTEGR21: 30;

        hence thesis by A38, A30, XXREAL_0: 2, A31;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A8);

      hence thesis;

    end;

    

     Lm8: for r,L,a,b,t be Real, m be Nat st a <= t & t <= b & 0 <= L & 0 <= r holds ((((r * (t - a)) |^ (m + 1)) / ((m + 1) ! )) * L) <= ((((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) * L)

    proof

      let r,L,a,b,t be Real, m be Nat;

      assume

       A1: a <= t & t <= b & 0 <= L & 0 <= r;

      then (t - a) <= (b - a) by XREAL_1: 13;

      then

       A2: (r * (t - a)) <= (r * (b - a)) by A1, XREAL_1: 64;

       0 <= (t - a) by A1, XREAL_1: 48;

      then

       A3: ((r * (t - a)) to_power (m + 1)) <= ((r * (b - a)) to_power (m + 1)) by A1, HOLDER_1: 3, A2;

      (((r * (t - a)) |^ (m + 1)) / ((m + 1) ! )) <= (((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) by A3, XREAL_1: 72;

      hence thesis by A1, XREAL_1: 64;

    end;

    

     Lm9: a < b & 0 < r implies ex m be Element of NAT st (((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) < 1 & 0 < (((r * (b - a)) |^ (m + 1)) / ((m + 1) ! ))

    proof

      assume

       A1: a < b & 0 < r;

      set z = (r * (b - a));

      set s = (z rExpSeq );

      s is summable by SIN_COS: 45;

      then s is convergent & ( lim s) = 0 by SERIES_1: 4;

      then

      consider n be Nat such that

       A3: for m be Nat st n <= m holds |.((s . m) - 0 ).| < 1 by SEQ_2:def 7;

      reconsider m0 = ( max (n,1)) as Element of NAT by ORDINAL1:def 12;

      reconsider m = (m0 - 1) as Element of NAT by INT_1: 5, XXREAL_0: 25;

      take m;

       |.((s . (m + 1)) - 0 ).| < 1 by A3, XXREAL_0: 25;

      then

       A4: |.(((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )).| < 1 by SIN_COS:def 5;

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

      then ( 0 qua Real * r) < (r * (b - a)) by A1, XREAL_1: 68;

      then 0 < ((r * (b - a)) to_power (m + 1)) by POWER: 34;

      hence thesis by A4, ABSVALUE:def 1, XREAL_1: 139;

    end;

    theorem :: ORDEQ_02:24

    

     Th55: for m be Nat st a <= b & 0 < r & (for y1,y2 be VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||)) holds for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) holds ||.((( iter (( Fredholm (G,a,b,y0)),(m + 1))) . u) - (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= ((((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||)

    proof

      let m be Nat;

      assume

       A1: a <= b & 0 < r & for y1,y2 be VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||);

      let u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

      reconsider u1 = (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . u) as VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

      reconsider v1 = (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . v) as VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

      consider g be continuous PartFunc of REAL , the carrier of X such that

       A2: u1 = g & ( dom g) = ['a, b'] by ORDEQ_01:def 2;

      consider h be continuous PartFunc of REAL , the carrier of X such that

       A3: v1 = h & ( dom h) = ['a, b'] by ORDEQ_01:def 2;

      now

        let t be Real;

        

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

        assume

         A5: t in ['a, b'];

        then

         A6: ex g be Real st t = g & a <= g & g <= b by A4;

        m in NAT by ORDINAL1:def 12;

        then

         A7: ||.((g /. t) - (h /. t)).|| <= ((((r * (t - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) by A5, Th54, A1, A2, A3;

        ((((r * (t - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) <= ((((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) by A6, A1, Lm8;

        hence ||.((g /. t) - (h /. t)).|| <= ((((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) by A7, XXREAL_0: 2;

      end;

      hence thesis by ORDEQ_01: 27, A2, A3;

    end;

    theorem :: ORDEQ_02:25

    

     Th56: a < b & G is_Lipschitzian_on the carrier of X implies ex m be Nat st ( iter (( Fredholm (G,a,b,y0)),(m + 1))) is contraction

    proof

      assume

       A1: a < b & G is_Lipschitzian_on the carrier of X;

      then

      consider r be Real such that

       A2: 0 < r & for x1,x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds ||.((G /. x1) - (G /. x2)).|| <= (r * ||.(x1 - x2).||);

      

       A3: for x1,x2 be Point of X holds ||.((G /. x1) - (G /. x2)).|| <= (r * ||.(x1 - x2).||) by A2;

      consider m be Element of NAT such that

       A4: (((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) < 1 & 0 < (((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) by Lm9, A1, A2;

      take m;

      for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) holds ||.((( iter (( Fredholm (G,a,b,y0)),(m + 1))) . u) - (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . v)).|| <= ((((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) by Th55, A3, A2, A1;

      hence thesis by A4;

    end;

    theorem :: ORDEQ_02:26

    

     Th57: a < b & G is_Lipschitzian_on the carrier of X implies ( Fredholm (G,a,b,y0)) is with_unique_fixpoint

    proof

      assume a < b & G is_Lipschitzian_on the carrier of X;

      then ex m be Nat st ( iter (( Fredholm (G,a,b,y0)),(m + 1))) is contraction by Th56;

      hence thesis by ORDEQ_01: 7;

    end;

    theorem :: ORDEQ_02:27

    

     Th58: for f,g be continuous PartFunc of REAL , the carrier of X st ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Z = ].a, b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (( Fredholm (G,a,b,y0)) . f) holds (g /. a) = y0 & g is_differentiable_on Z & for t be Real st t in Z holds ( diff (g,t)) = ((G * f) /. t)

    proof

      let f,g be continuous PartFunc of REAL , the carrier of X;

      assume

       A1: ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Z = ].a, b.[ & a < b & G is_Lipschitzian_on the carrier of X & g = (( Fredholm (G,a,b,y0)) . f);

      

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

      set D = ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

      

       X2: ( dom G) = the carrier of X by FUNCT_2:def 1;

      then

       A2: G is_continuous_on ( dom G) by A1, NFCONT_1: 45;

      f is Element of D by ORDEQ_01:def 2, A1;

      then

      consider f0,g0,Gf0 be continuous PartFunc of REAL , the carrier of X such that

       A3: f = f0 & (( Fredholm (G,a,b,y0)) . f) = g0 & ( dom f0) = ['a, b'] & ( dom g0) = ['a, b'] & Gf0 = (G * f0) & for t be Real st t in ['a, b'] holds (g0 /. t) = (y0 + ( integral (Gf0,a,t))) by A1, A2, Def8;

      reconsider Gf = (G * f) as continuous PartFunc of REAL , the carrier of X by A3;

      ( rng f) c= ( dom G) by X2;

      then ( dom Gf) = ['a, b'] by A1, RELAT_1: 27;

      hence thesis by A1, X1, Th40, Th40a, A3;

    end;

    theorem :: ORDEQ_02:28

    

     Th59: for y be continuous PartFunc of REAL , the carrier of X st a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of X & ( dom y) = ['a, b'] & y is_differentiable_on Z & (y /. a) = y0 & (for t be Real st t in Z holds ( diff (y,t)) = (G . (y /. t))) holds y is_a_fixpoint_of ( Fredholm (G,a,b,y0))

    proof

      let y be continuous PartFunc of REAL , the carrier of X;

      assume

       A1: a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of X & ( dom y) = ['a, b'] & y is_differentiable_on Z & (y /. a) = y0 & (for t be Real st t in Z holds ( diff (y,t)) = (G . (y /. t)));

      

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

      

       A2: ( dom ( Fredholm (G,a,b,y0))) = the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) by FUNCT_2:def 1;

      

       A3: y is Element of the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X)) by ORDEQ_01:def 2, A1;

      

       X2: ( dom G) = the carrier of X by FUNCT_2:def 1;

      then G is_continuous_on ( dom G) by A1, NFCONT_1: 45;

      then

      consider f,g,Gf be continuous PartFunc of REAL , the carrier of X such that

       A5: y = f & (( Fredholm (G,a,b,y0)) . y) = g & ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Gf = (G * f) & for t be Real st t in ['a, b'] holds (g /. t) = (y0 + ( integral (Gf,a,t))) by Def8, A1, A3;

      ( rng f) c= ( dom G) by X2;

      then

       A6: ( dom (G * f)) = ['a, b'] by A5, RELAT_1: 27;

      for t be Real st t in Z holds ( diff (y,t)) = (Gf /. t)

      proof

        let t be Real;

        assume

         A7: t in Z;

        

        hence ( diff (y,t)) = (G . (y /. t)) by A1

        .= (G . (y . t)) by A1, A7, PARTFUN1:def 6

        .= (Gf . t) by A5, A1, A7, FUNCT_1: 13

        .= (Gf /. t) by A5, A1, A7, A6, PARTFUN1:def 6;

      end;

      hence thesis by A1, X1, A2, A5, Th47, A6, ORDEQ_01:def 2;

    end;

    theorem :: ORDEQ_02:29

    for y1,y2 be continuous PartFunc of REAL , the carrier of X st a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of X & ( dom y1) = ['a, b'] & y1 is_differentiable_on Z & (y1 /. a) = y0 & (for t be Real st t in Z holds ( diff (y1,t)) = (G . (y1 /. t))) & ( dom y2) = ['a, b'] & y2 is_differentiable_on Z & (y2 /. a) = y0 & (for t be Real st t in Z holds ( diff (y2,t)) = (G . (y2 /. t))) holds y1 = y2

    proof

      let y1,y2 be continuous PartFunc of REAL , the carrier of X;

      assume

       A1: a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of X & ( dom y1) = ['a, b'] & y1 is_differentiable_on Z & (y1 /. a) = y0 & (for t be Real st t in Z holds ( diff (y1,t)) = (G . (y1 /. t))) & ( dom y2) = ['a, b'] & y2 is_differentiable_on Z & (y2 /. a) = y0 & (for t be Real st t in Z holds ( diff (y2,t)) = (G . (y2 /. t)));

      then ( Fredholm (G,a,b,y0)) is with_unique_fixpoint by Th57;

      then

      consider y be set such that

       SS: y is_a_fixpoint_of ( Fredholm (G,a,b,y0)) & for z be set st z is_a_fixpoint_of ( Fredholm (G,a,b,y0)) holds y = z;

      y1 = y by Th59, A1, SS

      .= y2 by Th59, A1, SS;

      hence thesis;

    end;

    theorem :: ORDEQ_02:30

    a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of X implies ex y be continuous PartFunc of REAL , the carrier of X st ( dom y) = ['a, b'] & y is_differentiable_on Z & (y /. a) = y0 & for t be Real st t in Z holds ( diff (y,t)) = (G . (y /. t))

    proof

      assume

       A1: a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of X;

      then ( Fredholm (G,a,b,y0)) is with_unique_fixpoint by Th57;

      then

      consider x be set such that

       A2: x is_a_fixpoint_of ( Fredholm (G,a,b,y0)) & for y be set st y is_a_fixpoint_of ( Fredholm (G,a,b,y0)) holds x = y;

      x in ( dom ( Fredholm (G,a,b,y0))) & x = (( Fredholm (G,a,b,y0)) . x) by A2;

      then

      reconsider x as Element of the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],X));

      consider f be continuous PartFunc of REAL , the carrier of X such that

       A4: x = f & ( dom f) = ['a, b'] by ORDEQ_01:def 2;

      take f;

      thus ( dom f) = ['a, b'] & f is_differentiable_on Z & (f /. a) = y0 by Th58, A4, A1, A2;

      

       A5: ].a, b.[ c= [.a, b.] by XXREAL_1: 25;

      

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

      let t be Real;

      assume

       A7: t in Z;

      ( dom G) = the carrier of X by FUNCT_2:def 1;

      then ( rng f) c= ( dom G);

      then

       A8: ( dom (G * f)) = ['a, b'] by A4, RELAT_1: 27;

      

      thus ( diff (f,t)) = ((G * f) /. t) by A7, Th58, A4, A1, A2

      .= ((G * f) . t) by A8, A5, A1, A7, A6, PARTFUN1:def 6

      .= (G . (f . t)) by A8, A5, A1, A7, A6, FUNCT_1: 12

      .= (G . (f /. t)) by A5, A1, A7, A6, A4, PARTFUN1:def 6;

    end;