ordeq_01.miz

    begin

    reserve n for non zero Element of NAT ;

    reserve a,b,r,t for Real;

    definition

      let f be Function;

      :: ORDEQ_01:def1

      attr f is with_unique_fixpoint means ex x be set st x is_a_fixpoint_of f & for y be set st y is_a_fixpoint_of f holds x = y;

    end

    theorem :: ORDEQ_01:1

    for x be set holds x is_a_fixpoint_of { [x, x]}

    proof

      let x be set;



       A1: [x, x] in { [x, x]} by TARSKI:def 1;

      ( dom { [x, x]}) = {x} by RELAT_1: 9;

      hence x in ( dom { [x, x]}) by TARSKI:def 1;

      hence x = ( { [x, x]} . x) by A1, FUNCT_1:def 2;

    end;

    theorem :: ORDEQ_01:2



     Th2: for x,y,z be set st x is_a_fixpoint_of { [y, z]} holds x = y

    proof

      let x,y,z be set;

      assume

       A1: x in ( dom { [y, z]});

      ( dom { [y, z]}) = {y} by RELAT_1: 9;

      hence thesis by A1, TARSKI:def 1;

    end;

    registration

      let x be set;

      cluster { [x, x]} -> with_unique_fixpoint;

      coherence

      proof

        set f = { [x, x]};



         A1: ( dom f) = {x} by RELAT_1: 9;

        take x;

        thus x is_a_fixpoint_of f

        proof

          thus

           A2: x in ( dom f) by A1, TARSKI:def 1;

           [x, x] in f by TARSKI:def 1;

          hence x = (f . x) by A2, FUNCT_1:def 2;

        end;

        let b be set;

        assume b is_a_fixpoint_of f;

        then b = x by Th2;

        hence thesis;

      end;

    end

    theorem :: ORDEQ_01:3



     Th3: for X be RealNormSpace, x be Point of X holds (for e be Real st e > 0 holds ||.x.|| < e) implies x = ( 0. X)

    proof

      let X be RealNormSpace, x be Point of X;

      assume

       A1: for e be Real st e > 0 holds ||.x.|| < e;

      assume x <> ( 0. X);

      then 0 <> ||.x.|| by NORMSP_0:def 5;

      hence contradiction by A1;

    end;

    theorem :: ORDEQ_01:4

    for X be RealNormSpace, x,y be Point of X holds (for e be Real st e > 0 holds ||.(x - y).|| < e) implies x = y

    proof

      let X be RealNormSpace, x,y be Point of X;

      assume for e be Real st e > 0 holds ||.(x - y).|| < e;

      then (x - y) = ( 0. X) by Th3;

      hence thesis by RLVECT_1: 21;

    end;

    theorem :: ORDEQ_01:5

    for K,L,e be Real st 0 < K & K < 1 & 0 < e holds ex n be Nat st |.(L * (K to_power n)).| < e

    proof

      let K,L,e be Real such that

       A1: 0 < K and

       A2: K < 1 and

       A3: 0 < e;

      deffunc P( Nat) = (K to_power ($1 + 1));

      consider rseq be Real_Sequence such that

       A4: for n be Nat holds (rseq . n) = P(n) from SEQ_1:sch 1;



       A5: (L (#) rseq) is convergent by A1, A2, A4, SEQ_2: 7, SERIES_1: 1;



       A6: ( lim (L (#) rseq)) = (L * ( lim rseq)) by A1, A2, A4, SEQ_2: 8, SERIES_1: 1

      .= (L * 0 qua Real) by A1, A2, A4, SERIES_1: 1;

      consider n be Nat such that

       A7: for m be Nat st n <= m holds |.(((L (#) rseq) . m) - 0 qua Real).| < e by A5, A6, A3, SEQ_2:def 7;

       |.(((L (#) rseq) . n) - 0 qua Real).| < e by A7;

      then |.(L * (rseq . n)).| < e by SEQ_1: 9;

      then |.(L * (K to_power (n + 1))).| < e by A4;

      hence thesis;

    end;

    registration

      let X be RealNormSpace;

      cluster constant -> contraction for Function of X, X;

      coherence

      proof

        let f be Function of X, X such that

         A1: f is constant;

        set K = (1 / 2);

        take K;

        thus 0 < K & K < 1;

        let x,y be Point of X;

        ( dom f) = the carrier of X by FUNCT_2:def 1;

        hence thesis by NORMSP_1: 6, A1, FUNCT_1:def 10;

      end;

    end

    registration

      let X be RealBanachSpace;

      cluster contraction -> with_unique_fixpoint for Function of X, X;

      coherence

      proof

        let f be Function of X, X;

        assume f is contraction;

        then

        consider xp be Point of X such that

         A1: (f . xp) = xp and

         A2: for x be Point of X st (f . x) = x holds xp = x by NFCONT_2: 14;

        take xp;

        thus (f . xp) = xp by A1;

        let y be set;

        assume y is_a_fixpoint_of f;

        then y in ( dom f) & (f . y) = y;

        hence thesis by A2;

      end;

    end

    ::$Canceled

    theorem :: ORDEQ_01:7



     Th7: for X be RealBanachSpace, f be Function of X, X st ex n0 be Nat st ( iter (f,n0)) is contraction holds f is with_unique_fixpoint

    proof

      let X be RealBanachSpace;

      let f be Function of X, X;

      given n0 be Nat such that

       A1: ( iter (f,n0)) is contraction;

      consider xp be Point of X such that

       A2: (( iter (f,n0)) . xp) = xp and

       A3: for x be Point of X st (( iter (f,n0)) . x) = x holds xp = x by A1, NFCONT_2: 14;

      take xp;

      thus

       A4: xp is_a_fixpoint_of f

      proof



         A5: (( iter (f,n0)) . (f . xp)) = ((( iter (f,n0)) * f) . xp) by FUNCT_2: 15

        .= (( iter (f,(n0 + 1))) . xp) by FUNCT_7: 69

        .= ((f * ( iter (f,n0))) . xp) by FUNCT_7: 71

        .= (f . xp) by A2, FUNCT_2: 15;

        thus (f . xp) = xp by A5, A3;

      end;

       A6:

      now

        let x be Point of X such that

         A7: (f . x) = x;

        for n be Nat holds (( iter (f,n)) . x) = x

        proof

          defpred P[ Nat] means (( iter (f,$1)) . x) = x;

          (( iter (f, 0 )) . x) = (( id the carrier of X) . x) by FUNCT_7: 84

          .= x;

          then

           A8: P[ 0 ];

           A9:

          now

            let n be Nat such that

             A10: P[n];

            reconsider m = n as Element of NAT by ORDINAL1:def 12;

            (( iter (f,(n + 1))) . x) = ((f * ( iter (f,m))) . x) by FUNCT_7: 71

            .= x by A7, A10, FUNCT_2: 15;

            hence P[(n + 1)];

          end;

          for n be Nat holds P[n] from NAT_1:sch 2( A8, A9);

          hence thesis;

        end;

        then (( iter (f,n0)) . x) = x;

        hence xp = x by A3;

      end;

      let y be set;



       A11: ( dom f) = the carrier of X by FUNCT_2:def 1;

      assume

       A12: y is_a_fixpoint_of f;

      then

      reconsider x1 = xp, y1 = y as Point of X by A11;



       A13: (f . x1) = x1 & (f . y1) = y1 by A12, A4;

      thus xp = y by A6, A13;

    end;

    theorem :: ORDEQ_01:8

    for X be RealBanachSpace, f be Function of X, X st ex n0 be Element of NAT st ( iter (f,n0)) is contraction holds ex xp be Point of X st (f . xp) = xp & for x be Point of X st (f . x) = x holds xp = x

    proof

      let X be RealBanachSpace;

      let f be Function of X, X;

      assume ex n0 be Element of NAT st ( iter (f,n0)) is contraction;

      then f is with_unique_fixpoint by Th7;

      then

      consider xp be set such that

       A1: xp is_a_fixpoint_of f & for y be set st y is_a_fixpoint_of f holds xp = y;

      xp in ( dom f) by A1;

      then

      reconsider xp as Point of X;

      take xp;

      thus (f . xp) = xp by A1;

      let x be Point of X;

      assume (f . x) = x;

      then x is_a_fixpoint_of f;

      hence xp = x by A1;

    end;

    begin

    theorem :: ORDEQ_01:9



     Th9: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f be continuous PartFunc of REAL , Y st ( dom f) = X holds f is bounded Function of X, Y

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let f be continuous PartFunc of REAL , Y;

      assume

       A1: ( dom f) = X;

      ( rng f) c= the carrier of Y;

      then

      reconsider g = f as Function of X, Y by A1, FUNCT_2: 2;

      (f | X) = f by A1;

      then

       A2: ( ||.f.|| | X) is continuous by A1, NFCONT_3: 22;



       A3: ( dom ||.f.||) = X by A1, NORMSP_0:def 2;

      then

      consider x1,x2 be Real such that

       A4: x1 in ( dom ||.f.||) & x2 in ( dom ||.f.||) & ( ||.f.|| . x1) = ( upper_bound ( rng ||.f.||)) & ( ||.f.|| . x2) = ( lower_bound ( rng ||.f.||)) by A2, FCONT_1: 30;



       A5: ( ||.f.|| . x1) = ||.(f /. x1).|| by A4, NORMSP_0:def 2;

      reconsider K = ( ||.f.|| . x1) as Real;

      now

        let x be Element of X;



         A6: ||.(g . x).|| = ||.(g /. x).||

        .= ( ||.f.|| . x) by A3, NORMSP_0:def 2

        .= ( ||.f.|| /. x) by A3, PARTFUN1:def 6;



         A7: ( rng ||.f.||) is real-bounded by A2, A3, FCONT_1: 28, RCOMP_1: 10;

        ( ||.f.|| . x) in ( rng ||.f.||) by A3, FUNCT_1: 3;

        then ( ||.f.|| /. x) in ( rng ||.f.||) by A3, PARTFUN1:def 6;

        hence ||.(g . x).|| <= K by A4, A6, A7, SEQ_4:def 1;

      end;

      hence thesis by A5, RSSPACE4:def 4;

    end;

    definition

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      :: ORDEQ_01:def2

      func ContinuousFunctions (X,Y) -> Subset of ( R_VectorSpace_of_BoundedFunctions (X,Y)) means

      : Def2: for x be set holds x in it iff ex f be continuous PartFunc of REAL , Y st x = f & ( dom f) = X;

      existence

      proof

        defpred P[ object] means ex f be continuous PartFunc of REAL , Y st $1 = f & ( dom f) = X;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( BoundedFunctions (X,Y)) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( BoundedFunctions (X,Y)) by A1;

        hence IT is Subset of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;

        let x be set;

        thus x in IT implies ex f be continuous PartFunc of REAL , Y st x = f & ( dom f) = X by A1;

        assume

         A2: ex f be continuous PartFunc of REAL , Y st x = f & ( dom f) = X;

        then

        consider f be continuous PartFunc of REAL , Y such that

         A3: x = f & ( dom f) = X;

        f is bounded Function of X, Y by A3, Th9;

        then x in ( BoundedFunctions (X,Y)) by A3, RSSPACE4:def 5;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( R_VectorSpace_of_BoundedFunctions (X,Y));

        assume that

         A4: for x be set holds x in X1 iff ex f be continuous PartFunc of REAL , Y st x = f & ( dom f) = X and

         A5: for x be set holds x in X2 iff ex f be continuous PartFunc of REAL , Y st x = f & ( dom f) = X;

        for x be object st x in X2 holds x in X1

        proof

          let x be object;

          assume x in X2;

          then ex f be continuous PartFunc of REAL , Y st x = f & ( dom f) = X by A5;

          hence thesis by A4;

        end;

        then

         A6: X2 c= X1 by TARSKI:def 3;

        for x be object st x in X1 holds x in X2

        proof

          let x be object;

          assume x in X1;

          then ex f be continuous PartFunc of REAL , Y st x = f & ( dom f) = X by A4;

          hence thesis by A5;

        end;

        then X1 c= X2 by TARSKI:def 3;

        hence thesis by A6, XBOOLE_0:def 10;

      end;

    end

    registration

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      cluster ( ContinuousFunctions (X,Y)) -> non empty;

      coherence

      proof

        set f = (X --> ( 0. Y));

        reconsider f as Function of X, Y;

        ( dom f) = X;

        then

        reconsider g = f as PartFunc of REAL , Y by RELSET_1: 5;

        ( dom g) = X;

        hence thesis by Def2;

      end;

    end

    registration

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace;

      cluster ( ContinuousFunctions (X,Y)) -> linearly-closed;

      coherence

      proof

        set W = ( ContinuousFunctions (X,Y));

        thus for v,u be VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) st v in W & u in W holds (v + u) in W

        proof

          let v,u be VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) such that

           A1: v in W and

           A2: u in W;

          reconsider f = (v + u), v0 = v, u0 = u as bounded Function of X, Y by RSSPACE4:def 5;

          consider v1 be continuous PartFunc of REAL , Y such that

           A3: v1 = v & ( dom v1) = X by A1, Def2;

          consider u1 be continuous PartFunc of REAL , Y such that

           A4: u1 = u & ( dom u1) = X by A2, Def2;



           A5: ( dom f) = (( dom v1) /\ ( dom u1)) by A3, A4, FUNCT_2:def 1;

           A6:

          now

            let x0 be Element of REAL ;

            assume

             A7: x0 in ( dom f);

            then

            reconsider x = x0 as Element of X;



            thus (f /. x0) = (f . x) by A7, PARTFUN1:def 6

            .= ((v0 /. x) + (u0 /. x)) by RSSPACE4: 8

            .= ((v1 /. x0) + (u1 /. x0)) by A3, A4;

          end;

          ( dom f) = X by FUNCT_2:def 1;

          then ( dom f) c= REAL & ( rng f) c= the carrier of Y;

          then f in ( PFuncs ( REAL ,the carrier of Y)) by PARTFUN1:def 3;

          then f is PartFunc of REAL , Y by PARTFUN1: 46;

          then

           A8: f = (v1 + u1) by A5, A6, VFUNCT_1:def 1;

          then ( dom (v1 + u1)) = X by FUNCT_2:def 1;

          hence thesis by Def2, A8;

        end;

        let a be Real;

        let v be VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) such that

         A9: v in W;

        reconsider f = (a * v), v0 = v as bounded Function of X, Y by RSSPACE4:def 5;

        consider v1 be continuous PartFunc of REAL , Y such that

         A10: v1 = v & ( dom v1) = X by A9, Def2;



         A11: ( dom f) = ( dom v1) by A10, FUNCT_2:def 1;

         A12:

        now

          let x0 be Element of REAL ;

          assume

           A13: x0 in ( dom f);

          then

          reconsider x = x0 as Element of X;



          thus (f /. x0) = (f . x) by A13, PARTFUN1:def 6

          .= (a * (v0 /. x)) by RSSPACE4: 9

          .= (a * (v1 /. x0)) by A10;

        end;

        ( dom f) = X by FUNCT_2:def 1;

        then ( dom f) c= REAL & ( rng f) c= the carrier of Y;

        then f in ( PFuncs ( REAL ,the carrier of Y)) by PARTFUN1:def 3;

        then f is PartFunc of REAL , Y by PARTFUN1: 46;

        then

         A14: f = (a (#) v1) by A11, A12, VFUNCT_1:def 4;

        then ( dom (a (#) v1)) = X by FUNCT_2:def 1;

        hence thesis by Def2, A14;

      end;

    end

    definition

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      :: ORDEQ_01:def3

      func R_VectorSpace_of_ContinuousFunctions (X,Y) -> strict RealLinearSpace equals RLSStruct (# ( ContinuousFunctions (X,Y)), ( Zero_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))), ( Add_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))), ( Mult_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))) #);

      coherence by RSSPACE: 11;

    end

    registration

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      cluster ( R_VectorSpace_of_ContinuousFunctions (X,Y)) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence ;

    end

    theorem :: ORDEQ_01:10



     Th10: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,g,h be VECTOR of ( R_VectorSpace_of_ContinuousFunctions (X,Y)), f9,g9,h9 be continuous PartFunc of REAL , Y st f9 = f & g9 = g & h9 = h & ( dom f9) = X & ( dom g9) = X & ( dom h9) = X holds (h = (f + g) iff for x be Element of X holds (h9 /. x) = ((f9 /. x) + (g9 /. x)))

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let f,g,h be VECTOR of ( R_VectorSpace_of_ContinuousFunctions (X,Y));



       A1: ( R_VectorSpace_of_ContinuousFunctions (X,Y)) is Subspace of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by RSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by RLSUB_1: 10;

      reconsider h1 = h as VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by A1, RLSUB_1: 10;

      reconsider g1 = g as VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by A1, RLSUB_1: 10;

      let f9,g9,h9 be continuous PartFunc of REAL , Y such that

       A2: f9 = f & g9 = g & h9 = h & ( dom f9) = X & ( dom g9) = X & ( dom h9) = X;

      reconsider f90 = f1, g90 = g1, h90 = h1 as bounded Function of X, Y by RSSPACE4:def 5;

       A3:

      now

        assume

         A4: h = (f + g);

        let x be Element of X;



         A5: h1 = (f1 + g1) by A1, A4, RLSUB_1: 13;



        thus (h9 /. x) = (h90 . x) by A2, PARTFUN1:def 6

        .= ((f90 /. x) + (g90 /. x)) by A5, RSSPACE4: 8

        .= ((f9 /. x) + (g9 /. x)) by A2;

      end;

      now

        assume

         A6: for x be Element of X holds (h9 /. x) = ((f9 /. x) + (g9 /. x));

        now

          let x be Element of X;



          thus (h90 . x) = (h9 /. x) by A2, PARTFUN1:def 6

          .= ((f90 /. x) + (g90 /. x)) by A2, A6

          .= ((f90 . x) + (g90 . x));

        end;

        then h1 = (f1 + g1) by RSSPACE4: 8;

        hence h = (f + g) by A1, RLSUB_1: 13;

      end;

      hence thesis by A3;

    end;

    theorem :: ORDEQ_01:11



     Th11: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,h be VECTOR of ( R_VectorSpace_of_ContinuousFunctions (X,Y)), f9,h9 be continuous PartFunc of REAL , Y st f9 = f & h9 = h & ( dom f9) = X & ( dom h9) = X holds h = (a * f) iff for x be Element of X holds (h9 /. x) = (a * (f9 /. x))

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let f,h be VECTOR of ( R_VectorSpace_of_ContinuousFunctions (X,Y));



       A1: ( R_VectorSpace_of_ContinuousFunctions (X,Y)) is Subspace of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by RSSPACE: 11;

      then

      reconsider f1 = f as VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by RLSUB_1: 10;

      reconsider h1 = h as VECTOR of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by A1, RLSUB_1: 10;

      let f9,h9 be continuous PartFunc of REAL , Y such that

       A2: f9 = f & h9 = h & ( dom f9) = X & ( dom h9) = X;

      reconsider f90 = f1 as bounded Function of X, Y by RSSPACE4:def 5;

      reconsider h90 = h1 as bounded Function of X, Y by RSSPACE4:def 5;

       A3:

      now

        assume

         A4: h = (a * f);

        let x be Element of X;



         A5: h1 = (a * f1) by A1, A4, RLSUB_1: 14;



        thus (h9 /. x) = (h90 . x) by A2, PARTFUN1:def 6

        .= (a * (f90 /. x)) by A5, RSSPACE4: 9

        .= (a * (f9 /. x)) by A2;

      end;

      now

        assume

         A6: for x be Element of X holds (h9 /. x) = (a * (f9 /. x));

        now

          let x be Element of X;



          thus (h90 . x) = (h9 /. x) by A2, PARTFUN1:def 6

          .= (a * (f90 /. x)) by A2, A6

          .= (a * (f90 . x));

        end;

        then h1 = (a * f1) by RSSPACE4: 9;

        hence h = (a * f) by A1, RLSUB_1: 14;

      end;

      hence thesis by A3;

    end;

    theorem :: ORDEQ_01:12



     Th12: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace holds ( 0. ( R_VectorSpace_of_ContinuousFunctions (X,Y))) = (X --> ( 0. Y))

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      ( R_VectorSpace_of_ContinuousFunctions (X,Y)) is Subspace of ( R_VectorSpace_of_BoundedFunctions (X,Y)) & ( 0. ( R_VectorSpace_of_BoundedFunctions (X,Y))) = (X --> ( 0. Y)) by RSSPACE4: 10, RSSPACE: 11;

      hence thesis by RLSUB_1: 11;

    end;

    definition

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      :: ORDEQ_01:def4

      func ContinuousFunctionsNorm (X,Y) -> Function of ( ContinuousFunctions (X,Y)), REAL equals (( BoundedFunctionsNorm (X,Y)) | ( ContinuousFunctions (X,Y)));

      correctness by FUNCT_2: 32;

    end

    definition

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let f be set;

      :: ORDEQ_01:def5

      func modetrans (f,X,Y) -> continuous PartFunc of REAL , Y means

      : Def5: it = f & ( dom it ) = X;

      correctness by A1, Def2;

    end

    definition

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      :: ORDEQ_01:def6

      func R_NormSpace_of_ContinuousFunctions (X,Y) -> strict non empty NORMSTR equals NORMSTR (# ( ContinuousFunctions (X,Y)), ( Zero_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))), ( Add_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))), ( Mult_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))), ( ContinuousFunctionsNorm (X,Y)) #);

      coherence ;

    end

    theorem :: ORDEQ_01:13

    for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f be continuous PartFunc of REAL , Y st ( dom f) = X holds ( modetrans (f,X,Y)) = f

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f be continuous PartFunc of REAL , Y;

      assume ( dom f) = X;

      then f in ( ContinuousFunctions (X,Y)) by Def2;

      hence thesis by Def5;

    end;

    theorem :: ORDEQ_01:14



     Th14: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace holds (X --> ( 0. Y)) = ( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y)))

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace;

      (X --> ( 0. Y)) = ( 0. ( R_VectorSpace_of_ContinuousFunctions (X,Y))) by Th12

      .= ( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y)));

      hence thesis;

    end;

    theorem :: ORDEQ_01:15



     Th15: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,g,h be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f9,g9,h9 be continuous PartFunc of REAL , Y st f9 = f & g9 = g & h9 = h & ( dom f9) = X & ( dom g9) = X & ( dom h9) = X holds (h = (f + g) iff for x be Element of X holds (h9 /. x) = ((f9 /. x) + (g9 /. x)))

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,g,h be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y));

      reconsider f1 = f, g1 = g, h1 = h as VECTOR of ( R_VectorSpace_of_ContinuousFunctions (X,Y));



       A1: h = (f + g) iff h1 = (f1 + g1);

      let f9,g9,h9 be continuous PartFunc of REAL , Y;

      thus thesis by A1, Th10;

    end;

    theorem :: ORDEQ_01:16

    for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,h be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f9,h9 be continuous PartFunc of REAL , Y st f9 = f & h9 = h & ( dom f9) = X & ( dom h9) = X holds (h = (a * f) iff for x be Element of X holds (h9 /. x) = (a * (f9 /. x)))

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,h be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y));

      reconsider f1 = f, h1 = h as VECTOR of ( R_VectorSpace_of_ContinuousFunctions (X,Y));

      let f9,h9 be continuous PartFunc of REAL , Y;

      assume

       A1: f9 = f & h9 = h & ( dom f9) = X & ( dom h9) = X;

      h = (a * f) iff h1 = (a * f1);

      hence thesis by A1, Th11;

    end;

    theorem :: ORDEQ_01:17



     Th17: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace, f be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) st f = g holds ||.f.|| = ||.g.|| by FUNCT_1: 49;

    theorem :: ORDEQ_01:18



     Th18: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace, f,g be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f1,g1 be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds (f + g) = (f1 + g1)

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,g be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f1,g1 be Point of ( R_NormSpace_of_BoundedFunctions (X,Y));

      assume

       A1: f1 = f & g1 = g;

      reconsider f2 = f, g2 = g as Point of ( R_VectorSpace_of_ContinuousFunctions (X,Y));

      reconsider f3 = f2, g3 = g2 as Point of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;



       A2: ( R_VectorSpace_of_ContinuousFunctions (X,Y)) is Subspace of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by RSSPACE: 11;



      thus (f + g) = (f2 + g2)

      .= (f3 + g3) by A2, RLSUB_1: 13

      .= (f1 + g1) by A1;

    end;

    theorem :: ORDEQ_01:19



     Th19: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace, f be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f1 be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds (a * f) = (a * f1)

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f1 be Point of ( R_NormSpace_of_BoundedFunctions (X,Y));

      assume

       A1: f1 = f;

      reconsider f2 = f as Point of ( R_VectorSpace_of_ContinuousFunctions (X,Y));

      reconsider f3 = f2 as Point of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;



       A2: ( R_VectorSpace_of_ContinuousFunctions (X,Y)) is Subspace of ( R_VectorSpace_of_BoundedFunctions (X,Y)) by RSSPACE: 11;



      thus (a * f) = (a * f2)

      .= (a * f3) by A2, RLSUB_1: 14

      .= (a * f1) by A1;

    end;



     Lm2: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace holds for f,g be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)) holds ( ||.f.|| = 0 iff f = ( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y)))) & ||.(a * f).|| = ( |.a.| * ||.f.||) & ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let f,g be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y));

      reconsider f1 = f as VECTOR of ( R_NormSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;

      reconsider g1 = g as VECTOR of ( R_NormSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;



       A1: ( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y))) = (X --> ( 0. Y)) by Th14

      .= ( 0. ( R_NormSpace_of_BoundedFunctions (X,Y))) by RSSPACE4: 15;



       A2: ||.(f1 + g1).|| <= ( ||.f1.|| + ||.g1.||) by RSSPACE4: 21;



       A3: ||.(f1 + g1).|| = ||.(f + g).|| by Th18, Th17;



       A4: ||.f1.|| = ||.f.|| by FUNCT_1: 49;

       ||.(a * f1).|| = ||.(a * f).|| by Th19, Th17;

      hence thesis by RSSPACE4: 21, A1, FUNCT_1: 49, A2, A3, A4;

    end;



     Lm3: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace holds ( R_NormSpace_of_ContinuousFunctions (X,Y)) is reflexive discerning RealNormSpace-like

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      thus ||.( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y))).|| = 0 by Lm2;

      for x,y be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)) holds for a be Real holds ( ||.x.|| = 0 iff x = ( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y)))) & ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Lm2;

      hence thesis by NORMSP_1:def 1;

    end;



     Lm4: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace holds ( R_NormSpace_of_ContinuousFunctions (X,Y)) is RealNormSpace

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

       RLSStruct (# ( ContinuousFunctions (X,Y)), ( Zero_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))), ( Add_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))), ( Mult_ (( ContinuousFunctions (X,Y)),( R_VectorSpace_of_BoundedFunctions (X,Y)))) #) is RealLinearSpace by RSSPACE: 11;

      hence thesis by Lm3, RSSPACE3: 2;

    end;

    registration

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      cluster ( R_NormSpace_of_ContinuousFunctions (X,Y)) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence by Lm4;

    end

    theorem :: ORDEQ_01:20



     Th20: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace holds for f,g,h be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)) holds for f9,g9,h9 be continuous PartFunc of REAL , Y st f9 = f & g9 = g & h9 = h & ( dom f9) = X & ( dom g9) = X & ( dom h9) = X holds (h = (f - g) iff for x be Element of X holds (h9 /. x) = ((f9 /. x) - (g9 /. x)))

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let f,g,h be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y));

      let f9,g9,h9 be continuous PartFunc of REAL , Y such that

       A1: f9 = f & g9 = g & h9 = h & ( dom f9) = X & ( dom g9) = X & ( dom h9) = X;

       A2:

      now

        assume

         A3: for x be Element of X holds (h9 /. x) = ((f9 /. x) - (g9 /. x));

        now

          let x be Element of X;

          (h9 /. x) = ((f9 /. x) - (g9 /. x)) by A3;

          then ((h9 /. x) + (g9 /. x)) = ((f9 /. x) - ((g9 /. x) - (g9 /. x))) by RLVECT_1: 29;

          then ((h9 /. x) + (g9 /. x)) = ((f9 /. x) - ( 0. Y)) by RLVECT_1: 15;

          hence ((h9 /. x) + (g9 /. x)) = (f9 /. x);

        end;

        then f = (h + g) by A1, Th15;

        then (f - g) = (h + (g - g)) by RLVECT_1:def 3;

        then (f - g) = (h + ( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y)))) by RLVECT_1: 5;

        hence (f - g) = h;

      end;

      now

        assume h = (f - g);

        then (h + g) = (f - (g - g)) by RLVECT_1: 29;

        then

         A4: (h + g) = (f - ( 0. ( R_NormSpace_of_ContinuousFunctions (X,Y)))) by RLVECT_1: 5;

        now

          let x be Element of X;

          (f9 /. x) = ((h9 /. x) + (g9 /. x)) by A1, A4, Th15;

          then ((f9 /. x) - (g9 /. x)) = ((h9 /. x) + ((g9 /. x) - (g9 /. x))) by RLVECT_1:def 3;

          then ((f9 /. x) - (g9 /. x)) = ((h9 /. x) + ( 0. Y)) by RLVECT_1: 15;

          hence ((f9 /. x) - (g9 /. x)) = (h9 /. x);

        end;

        hence for x be Element of X holds (h9 /. x) = ((f9 /. x) - (g9 /. x));

      end;

      hence thesis by A2;

    end;

    theorem :: ORDEQ_01:21



     Th21: for X be non empty closed_interval Subset of REAL holds for Y be RealNormSpace, f,g be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f1,g1 be Point of ( R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds (f - g) = (f1 - g1)

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, f,g be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), f1,g1 be Point of ( R_NormSpace_of_BoundedFunctions (X,Y));

      assume

       A1: f1 = f & g1 = g;



       A2: ( - g1) = (( - 1) * g1) by RLVECT_1: 16

      .= (( - 1) * g) by A1, Th19

      .= ( - g) by RLVECT_1: 16;

      thus (f - g) = (f1 - g1) by A1, A2, Th18;

    end;



     Lm5: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, C be Subset of ( R_NormSpace_of_BoundedFunctions (X,Y)) st C = ( ContinuousFunctions (X,Y)) holds C is closed

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let C be Subset of ( R_NormSpace_of_BoundedFunctions (X,Y));

      assume

       A1: C = ( ContinuousFunctions (X,Y));

      now

        let seq be sequence of ( R_NormSpace_of_BoundedFunctions (X,Y));

        assume

         A2: ( rng seq) c= C & seq is convergent;

        reconsider f = ( lim seq) as bounded Function of X, Y by RSSPACE4:def 5;



         A3: ( dom f) = X by FUNCT_2:def 1;

        now

          let z be object;

          assume z in ( BoundedFunctions (X,Y));

          then z is bounded Function of X, Y by RSSPACE4:def 5;

          hence z in ( PFuncs (X,the carrier of Y)) by PARTFUN1: 45;

        end;

        then ( BoundedFunctions (X,Y)) c= ( PFuncs (X,the carrier of Y)) by TARSKI:def 3;

        then

        reconsider H = seq as Functional_Sequence of X, the carrier of Y by FUNCT_2: 7;



         A4: for p be Real st p > 0 holds ex k be Nat st for n be Nat, x be set st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p

        proof

          let p be Real;

          assume p > 0 ;

          then

          consider k be Nat such that

           A5: for n be Nat st n >= k holds ||.((seq . n) - ( lim seq)).|| < p by A2, NORMSP_1:def 7;

          take k;

          hereby

            let n be Nat, x be set;

            assume

             A6: n >= k & x in X;

            then

             A7: ||.((seq . n) - ( lim seq)).|| < p by A5;

            reconsider g = ((seq . n) - ( lim seq)), s = (seq . n) as bounded Function of X, Y by RSSPACE4:def 5;

            reconsider x0 = x as Element of X by A6;



             A8: (g . x0) = ((s /. x0) - (f /. x0)) by RSSPACE4: 24;

             ||.(g . x0).|| <= ||.((seq . n) - ( lim seq)).|| by RSSPACE4: 16;

            hence ||.(((H . n) /. x) - (f /. x)).|| < p by A8, A7, XXREAL_0: 2;

          end;

        end;

        ( dom f) = X by FUNCT_2:def 1;

        then ( dom f) c= REAL & ( rng f) c= the carrier of Y;

        then f in ( PFuncs ( REAL ,the carrier of Y)) by PARTFUN1:def 3;

        then

        reconsider f as PartFunc of REAL , Y by PARTFUN1: 46;

        for x0 be Real st x0 in ( dom f) holds f is_continuous_in x0

        proof

          let x be Real;

          assume

           A9: x in ( dom f);

          now

            let r0 be Real;

            assume

             A10: 0 < r0;

            then

            consider k be Nat such that

             A11: for n be Nat, x be set st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < (r0 / 3) by A4, XREAL_1: 222;



             A12: ||.(((H . k) /. x) - (f /. x)).|| < (r0 / 3) by A11, A3, A9;

            k in NAT by ORDINAL1:def 12;

            then k in ( dom seq) by NORMSP_1: 12;

            then (H . k) in ( rng seq) by FUNCT_1:def 3;

            then

            consider h be continuous PartFunc of REAL , Y such that

             A13: (H . k) = h & ( dom h) = X by A2, Def2, A1;



             A14: 0 < (r0 / 3) & (r0 / 3) is Real by A10, XREAL_1: 222;

            x in ( dom h) by A9, A13, FUNCT_2:def 1;

            then h is_continuous_in x by NFCONT_3:def 2;

            then

            consider w1 be Real such that

             A15: 0 < w1 & for x0 be Real st x0 in ( dom h) & |.(x0 - x).| < w1 holds ||.((h /. x0) - (h /. x)).|| < (r0 / 3) by A14, NFCONT_3: 8;

            take w1;

            thus 0 < w1 by A15;

            thus for z0 be Real st z0 in ( dom f) & |.(z0 - x).| < w1 holds ||.((f /. z0) - (f /. x)).|| < r0

            proof

              let z0 be Real;

              assume

               A16: z0 in ( dom f) & |.(z0 - x).| < w1;

              then

               A17: z0 in ( dom h) by FUNCT_2:def 1, A13;

              then

               A18: ||.((h /. z0) - (h /. x)).|| < (r0 / 3) by A16, A15;



               A19: ||.((f /. x) - (h /. x)).|| < (r0 / 3) by A12, A13, NORMSP_1: 7;

               ||.((h /. z0) - (f /. z0)).|| < (r0 / 3) by A17, A11, A13;

              then ||.((f /. z0) - (h /. z0)).|| < (r0 / 3) by NORMSP_1: 7;

              then ( ||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) < ((r0 / 3) + (r0 / 3)) by A19, XREAL_1: 8;

              then

               A20: (( ||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) + ||.((h /. z0) - (h /. x)).||) < (((r0 / 3) + (r0 / 3)) + (r0 / 3)) by A18, XREAL_1: 8;

              ((((f /. z0) - (h /. z0)) - ((f /. x) - (h /. x))) + ((h /. z0) - (h /. x))) = (((f /. z0) - (h /. z0)) - (((f /. x) - (h /. x)) - ((h /. z0) - (h /. x)))) by RLVECT_1: 29

              .= (((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. x) + ((h /. z0) - (h /. x))))) by RLVECT_1: 27

              .= (((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. z0) - ((h /. x) - (h /. x))))) by RLVECT_1: 29

              .= (((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. z0) - ( 0. Y)))) by RLVECT_1: 15

              .= ((f /. z0) - ((h /. z0) + ((f /. x) - (h /. z0)))) by RLVECT_1: 27

              .= ((f /. z0) - ((f /. x) - ((h /. z0) - (h /. z0)))) by RLVECT_1: 29

              .= ((f /. z0) - ((f /. x) - ( 0. Y))) by RLVECT_1: 15

              .= ((f /. z0) - (f /. x));

              then

               A21: ||.((f /. z0) - (f /. x)).|| <= ( ||.(((f /. z0) - (h /. z0)) - ((f /. x) - (h /. x))).|| + ||.((h /. z0) - (h /. x)).||) by NORMSP_1:def 1;

              ( ||.(((f /. z0) - (h /. z0)) - ((f /. x) - (h /. x))).|| + ||.((h /. z0) - (h /. x)).||) <= (( ||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) + ||.((h /. z0) - (h /. x)).||) by XREAL_1: 6, NORMSP_1: 3;

              then ||.((f /. z0) - (f /. x)).|| <= (( ||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) + ||.((h /. z0) - (h /. x)).||) by A21, XXREAL_0: 2;

              hence ||.((f /. z0) - (f /. x)).|| < r0 by A20, XXREAL_0: 2;

            end;

          end;

          hence f is_continuous_in x by A9, NFCONT_3: 8;

        end;

        then f is continuous by NFCONT_3:def 2;

        hence ( lim seq) in C by A3, Def2, A1;

      end;

      hence thesis by NFCONT_1:def 3;

    end;

    registration

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace;

      cluster closed for Subset of ( R_NormSpace_of_BoundedFunctions (X,Y));

      existence

      proof

        reconsider C = ( ContinuousFunctions (X,Y)) as Subset of ( R_NormSpace_of_BoundedFunctions (X,Y));

        C is closed by Lm5;

        hence thesis;

      end;

    end

    theorem :: ORDEQ_01:22



     Th22: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace holds ( ContinuousFunctions (X,Y)) is closed Subset of ( R_NormSpace_of_BoundedFunctions (X,Y)) by Lm5;

    theorem :: ORDEQ_01:23



     Th23: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, seq be sequence of ( R_NormSpace_of_ContinuousFunctions (X,Y)) st Y is complete & seq is Cauchy_sequence_by_Norm holds seq is convergent

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealNormSpace;

      let vseq be sequence of ( R_NormSpace_of_ContinuousFunctions (X,Y));

      assume

       A1: Y is complete & vseq is Cauchy_sequence_by_Norm;

      ( rng vseq) c= ( BoundedFunctions (X,Y)) by XBOOLE_1: 1;

      then

      reconsider vseq1 = vseq as sequence of ( R_NormSpace_of_BoundedFunctions (X,Y)) by FUNCT_2: 6;

      now

        let e be Real such that

         A2: e > 0 ;

        consider k be Nat such that

         A3: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A1, A2, RSSPACE3: 8;

        take k;

        now

          let n,m be Nat;

          assume n >= k & m >= k;

          then ||.((vseq . n) - (vseq . m)).|| < e by A3;

          hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Th17, Th21;

        end;

        hence for n,m be Nat st n >= k & m >= k holds ||.((vseq1 . n) - (vseq1 . m)).|| < e;

      end;

      then

       A4: vseq1 is convergent by A1, LOPBAN_1:def 15, RSSPACE3: 8;

      reconsider Z = ( ContinuousFunctions (X,Y)) as Subset of ( R_NormSpace_of_BoundedFunctions (X,Y));

      ( rng vseq) c= ( ContinuousFunctions (X,Y));

      then

      reconsider tv = ( lim vseq1) as Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)) by A4, NFCONT_1:def 3, Th22;

      for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds ||.((vseq . n) - tv).|| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

         A5: for n be Nat st n >= k holds ||.((vseq1 . n) - ( lim vseq1)).|| < e by A4, NORMSP_1:def 7;

        take k;

        now

          let n be Nat;

          assume n >= k;

          then ||.((vseq1 . n) - ( lim vseq1)).|| < e by A5;

          hence ||.((vseq . n) - tv).|| < e by Th17, Th21;

        end;

        hence for n be Nat st n >= k holds ||.((vseq . n) - tv).|| < e;

      end;

      hence thesis by NORMSP_1:def 6;

    end;



     Lm6: for X be non empty closed_interval Subset of REAL , Y be RealBanachSpace holds ( R_NormSpace_of_ContinuousFunctions (X,Y)) is RealBanachSpace

    proof

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealBanachSpace;

      for seq be sequence of ( R_NormSpace_of_ContinuousFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th23;

      hence thesis by LOPBAN_1:def 15;

    end;

    registration

      let X be non empty closed_interval Subset of REAL ;

      let Y be RealBanachSpace;

      cluster ( R_NormSpace_of_ContinuousFunctions (X,Y)) -> complete;

      coherence by Lm6;

    end

    theorem :: ORDEQ_01:24



     Th24: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, v be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g be PartFunc of REAL , Y st g = v holds for t be Real st t in X holds ||.(g /. t).|| <= ||.v.||

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, v be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g be PartFunc of REAL , Y;

      assume

       A1: g = v;

      consider f be continuous PartFunc of REAL , Y such that

       A2: v = f & ( dom f) = X by Def2;

      reconsider g1 = g as bounded Function of X, Y by A1, Th9, A2;

      reconsider v1 = v as VECTOR of ( R_NormSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;



       A3: ||.v1.|| = ||.v.|| by FUNCT_1: 49;

      let t be Real;

      assume t in X;

      then

      reconsider t1 = t as Element of X;

       ||.(g1 . t1).|| <= ||.v1.|| by A1, RSSPACE4: 16;

      hence thesis by A2, A1, PARTFUN1:def 6, A3;

    end;

    theorem :: ORDEQ_01:25



     Th25: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, K be Real, v be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g be PartFunc of REAL , Y st g = v & for t be Real st t in X holds ||.(g /. t).|| <= K holds ||.v.|| <= K

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, K be Real, v be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g be PartFunc of REAL , Y;

      assume

       A1: g = v & for t be Real st t in X holds ||.(g /. t).|| <= K;

      consider f be continuous PartFunc of REAL , Y such that

       A2: v = f & ( dom f) = X by Def2;

      reconsider g1 = g as bounded Function of X, Y by A1, Th9, A2;

      reconsider v1 = v as VECTOR of ( R_NormSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;



       A3: for t be Element of X holds ||.(g1 . t).|| <= K

      proof

        let t be Element of X;

        reconsider t1 = t as Real;

         ||.(g /. t1).|| <= K by A1;

        hence ||.(g1 . t).|| <= K by A2, A1, PARTFUN1:def 6;

      end;



       A4: for x be Element of REAL st x in ( PreNorms g1) holds x <= K

      proof

        let x be Element of REAL ;

        assume x in ( PreNorms g1);

        then

        consider t be Element of X such that

         A5: x = ||.(g1 . t).||;

        thus thesis by A3, A5;

      end;

      ( upper_bound ( PreNorms g1)) <= K

      proof

        assume

         A6: not ( upper_bound ( PreNorms g1)) <= K;

        reconsider s = (( upper_bound ( PreNorms g1)) - K) as Real;



         A7: 0 < s by A6, XREAL_1: 50;

        ( PreNorms g1) is non empty bounded_above by RSSPACE4: 11;

        then

        consider r be Real such that

         A8: r in ( PreNorms g1) & (( upper_bound ( PreNorms g1)) - s) < r by A7, SEQ_4:def 1;

        thus contradiction by A8, A4;

      end;

      then ||.v1.|| <= K by A1, RSSPACE4: 14;

      hence thesis by FUNCT_1: 49;

    end;

    theorem :: ORDEQ_01:26



     Th26: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, v1,v2 be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g1,g2 be PartFunc of REAL , Y st g1 = v1 & g2 = v2 holds for t be Real st t in X holds ||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).||

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, v1,v2 be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g1,g2 be PartFunc of REAL , Y;

      assume

       A1: g1 = v1 & g2 = v2;

      consider f1 be continuous PartFunc of REAL , Y such that

       A2: v1 = f1 & ( dom f1) = X by Def2;

      consider f2 be continuous PartFunc of REAL , Y such that

       A3: v2 = f2 & ( dom f2) = X by Def2;

      consider f12 be continuous PartFunc of REAL , Y such that

       A4: (v1 - v2) = f12 & ( dom f12) = X by Def2;

      let t be Real;

      assume t in X;

      then

      reconsider t1 = t as Element of X;

      (f12 /. t1) = ((f1 /. t1) - (f2 /. t1)) by A2, A3, A4, Th20;

      hence ||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).|| by A1, A2, A3, A4, Th24;

    end;

    theorem :: ORDEQ_01:27



     Th27: for X be non empty closed_interval Subset of REAL , Y be RealNormSpace, K be Real, v1,v2 be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g1,g2 be PartFunc of REAL , Y st g1 = v1 & g2 = v2 & for t be Real st t in X holds ||.((g1 /. t) - (g2 /. t)).|| <= K holds ||.(v1 - v2).|| <= K

    proof

      let X be non empty closed_interval Subset of REAL , Y be RealNormSpace, K be Real, v1,v2 be Point of ( R_NormSpace_of_ContinuousFunctions (X,Y)), g1,g2 be PartFunc of REAL , Y;

      assume

       A1: g1 = v1 & g2 = v2 & for t be Real st t in X holds ||.((g1 /. t) - (g2 /. t)).|| <= K;

      consider f1 be continuous PartFunc of REAL , Y such that

       A2: v1 = f1 & ( dom f1) = X by Def2;

      consider f2 be continuous PartFunc of REAL , Y such that

       A3: v2 = f2 & ( dom f2) = X by Def2;

      consider f12 be continuous PartFunc of REAL , Y such that

       A4: (v1 - v2) = f12 & ( dom f12) = X by Def2;

      for t be Real st t in X holds ||.(f12 /. t).|| <= K

      proof

        let t be Real;

        assume t in X;

        then

        reconsider t1 = t as Element of X;

        (f12 /. t1) = ((g1 /. t) - (g2 /. t)) by A1, A2, A3, A4, Th20;

        hence ||.(f12 /. t).|| <= K by A1;

      end;

      hence thesis by Th25, A4;

    end;

    begin

    theorem :: ORDEQ_01:28



     Th28: for n,i be Nat, f be PartFunc of REAL , ( REAL n), A be Subset of REAL holds (( proj (i,n)) * (f | A)) = ((( proj (i,n)) * f) | A)

    proof

      let n,i be Nat, f be PartFunc of REAL , ( REAL n), A be Subset of REAL ;



       A1: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

      then

       A2: ( rng f) c= ( dom ( proj (i,n)));



       A3: ( rng (f | A)) c= ( dom ( proj (i,n))) by A1;

       A4:

      now

        let c be object;

        assume

         A5: c in ( dom ((( proj (i,n)) * f) | A));

        then

         A6: c in (( dom (( proj (i,n)) * f)) /\ A) by RELAT_1: 61;



         A7: c in ( dom (( proj (i,n)) * f)) by A6, XBOOLE_0:def 4;

        then c in ( dom f) by A2, RELAT_1: 27;

        then c in (( dom f) /\ A) by A5, XBOOLE_0:def 4;

        then

         A8: c in ( dom (f | A)) by RELAT_1: 61;

        then c in ( dom (( proj (i,n)) * (f | A))) by A3, RELAT_1: 27;



        then ((( proj (i,n)) * (f | A)) . c) = (( proj (i,n)) . ((f | A) . c)) by FUNCT_1: 12

        .= (( proj (i,n)) . (f . c)) by A8, FUNCT_1: 47

        .= ((( proj (i,n)) * f) . c) by A7, FUNCT_1: 12;

        hence (((( proj (i,n)) * f) | A) . c) = ((( proj (i,n)) * (f | A)) . c) by A5, FUNCT_1: 47;

      end;

      ( dom ((( proj (i,n)) * f) | A)) = (( dom (( proj (i,n)) * f)) /\ A) by RELAT_1: 61

      .= (( dom f) /\ A) by A2, RELAT_1: 27

      .= ( dom (f | A)) by RELAT_1: 61

      .= ( dom (( proj (i,n)) * (f | A))) by A3, RELAT_1: 27;

      hence thesis by A4, FUNCT_1: 2;

    end;

    theorem :: ORDEQ_01:29



     Th29: for g be continuous PartFunc of REAL , ( REAL n) st ( dom g) = ['a, b'] holds (g | ['a, b']) is bounded

    proof

      let g be continuous PartFunc of REAL , ( REAL n);

      assume

       A1: ( dom g) = ['a, b'];



       A2: for i be Element of NAT st i in ( Seg n) holds ((( proj (i,n)) * g) | ['a, b']) is continuous

      proof

        let i be Element of NAT ;

        assume i in ( Seg n);

        then (( proj (i,n)) * g) is continuous by NFCONT_4: 44;

        hence ((( proj (i,n)) * g) | ['a, b']) is continuous;

      end;

      let i be Element of NAT ;

      assume

       A3: i in ( Seg n);

      ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

      then ( rng g) c= ( dom ( proj (i,n)));

      then ['a, b'] c= ( dom (( proj (i,n)) * g)) by A1, RELAT_1: 27;

      then ((( proj (i,n)) * g) | ['a, b']) is bounded by A3, A2, INTEGRA5: 10;

      hence thesis by Th28;

    end;

    theorem :: ORDEQ_01:30



     Th30: for g be continuous PartFunc of REAL , ( REAL n) st ( dom g) = ['a, b'] holds g is_integrable_on ['a, b']

    proof

      let g be continuous PartFunc of REAL , ( REAL n);

      assume

       A1: ( dom g) = ['a, b'];

      let i be Element of NAT ;

      assume i in ( Seg n);

      then

       A2: (( proj (i,n)) * g) is continuous by NFCONT_4: 44;

      ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

      then ( rng g) c= ( dom ( proj (i,n)));

      then

       A3: ['a, b'] c= ( dom (( proj (i,n)) * g)) by A1, RELAT_1: 27;

      ((( proj (i,n)) * g) | ['a, b']) is continuous by A2;

      hence thesis by A3, INTEGRA5: 11;

    end;

    theorem :: ORDEQ_01:31



     Th31: for f,F be PartFunc of REAL , ( REAL n) st a <= b & ( dom f) = ['a, b'] & ( dom F) = ['a, b'] & f is continuous & 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,F be PartFunc of REAL , ( REAL n);

      assume

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



       A2: (f | ['a, b']) is bounded by A1, Th29;

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

      then ( |.f.| | ['a, b']) = |.f.| by A1;

      then |.f.| is bounded by A1, A2, INTEGR19: 19;

      then

      consider K be Real such that

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

      a in [.a, b.] by A1;

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

      then a in ( dom |.f.|) by A1, NFCONT_4:def 2;

      then

       A4: |.( |.f.| . a).| < K by A3;



       A5: 0 < K by A4, COMPLEX1: 46;

       A6:

      now

        let c,d be Real;

        assume

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

        let y be Real;

        assume

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

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

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

        then

         A9: y in ( dom |.f.|) by NFCONT_4:def 2, A1;

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

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

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

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

      end;

       A10:

      now

        let c,d be Real;

        assume

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

        then for y be Real st y in ['( min (c,d)), ( max (c,d))'] holds |.(f /. y).| <= K by A6;

        hence |.( integral (f,c,d)).| <= ((n * K) * |.(d - c).|) by A1, A2, Th30, A11, INTEGR19: 32;

      end;

      let x0 be Real;

      assume

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

      then

       A13: x0 in ( dom F) by INTEGRA5:def 3, A1;

      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

         A14: 0 < r;



         A15: 0 < (n * K) by A5, XREAL_1: 129;

        then

        consider s be Real such that

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

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

        then

         A17: 0 < s & ((n * K) * s) < r by A15, XCMPLX_1: 87, A16;

        take s;

        thus 0 < s by A16;

        let x1 be Real;

        assume

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

        then

         A19: x0 in ['a, b'] & x1 in ['a, b'] by A1, A12, INTEGRA5:def 3;

        then

         A20: |.( integral (f,x0,x1)).| <= ((n * K) * |.(x1 - x0).|) by A10;

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

        then

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



         A22: x0 in [.a, b.] & x1 in [.a, b.] by A1, A12, INTEGRA5:def 3, A18;



         A23: (F /. x0) = (F . x0) by A19, A1, PARTFUN1:def 6

        .= ( integral (f,a,x0)) by A1, A12;



         A24: (F /. x1) = (F . x1) by A18, PARTFUN1:def 6

        .= ( integral (f,a,x1)) by A22, A1;

        reconsider R1 = (F /. x0) as Element of (n -tuples_on REAL );

        reconsider R2 = ( integral (f,x0,x1)) as Element of (n -tuples_on REAL );

        (((F /. x0) + ( integral (f,x0,x1))) - (F /. x0)) = ( integral (f,x0,x1)) by RVSUM_1: 42;

        then |.((F /. x1) - (F /. x0)).| <= ((n * K) * |.(x1 - x0).|) by A24, A23, A2, Th30, A19, A1, INTEGR19: 31, A20;

        hence thesis by A21, XXREAL_0: 2;

      end;

      hence F is_continuous_in x0 by A13, NFCONT_4: 3;

    end;

    theorem :: ORDEQ_01:32



     Th32: for f be continuous PartFunc of REAL , ( REAL-NS n) st ( dom f) = ['a, b'] holds (f | ['a, b']) is bounded

    proof

      let f be continuous PartFunc of REAL , ( REAL-NS n);

      assume

       A1: ( dom f) = ['a, b'];

      reconsider g = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;

      g is continuous by NFCONT_4: 23;

      then (g | ['a, b']) is bounded by A1, Th29;

      hence (f | ['a, b']) is bounded by INTEGR19: 34;

    end;

    theorem :: ORDEQ_01:33



     Th33: for f be continuous PartFunc of REAL , ( REAL-NS n) st ( dom f) = ['a, b'] holds f is_integrable_on ['a, b']

    proof

      let f be continuous PartFunc of REAL , ( REAL-NS n);

      assume

       A1: ( dom f) = ['a, b'];

      reconsider g = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;



       A2: g is continuous by NFCONT_4: 23;

      then

       A3: g is_integrable_on ['a, b'] by A1, Th30;

      (g | ['a, b']) is bounded by A2, A1, Th29;

      hence thesis by A1, A3, INTEGR19: 44;

    end;

    theorem :: ORDEQ_01:34



     Th34: for f be continuous PartFunc of REAL , ( REAL-NS n), F be PartFunc of REAL , ( REAL-NS n) st a <= b & ( 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 continuous PartFunc of REAL , ( REAL-NS n), F be PartFunc of REAL , ( REAL-NS n);

      assume

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

      reconsider f0 = f, F0 = F as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;



       A2: (f | ['a, b']) is bounded by A1, Th32;

      a in [.a, b.] by A1;

      then

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



       A4: f0 is continuous by NFCONT_4: 23;

       A5:

      now

        let t be Real;

        assume

         A6: t in [.a, b.];

        then

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



        thus (F0 . t) = ( integral (f,a,t)) by A1, A6

        .= ( integral (f0,a,t)) by A1, A7, A2, Th33, A3, INTEGR19: 48;

      end;

      now

        let x be Real;

        assume x in [.a, b.];

        then F0 is_continuous_in x by A4, A5, A1, Th31;

        hence F is_continuous_in x by NFCONT_4: 1;

      end;

      hence thesis;

    end;

    theorem :: ORDEQ_01:35



     Th35: for R be PartFunc of REAL , REAL st R is total holds R is RestFunc-like iff for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds (( |.z.| " ) * |.(R /. z).|) < r

    proof

      let R be PartFunc of REAL , REAL such that

       A1: R is total;

      thus R is RestFunc-like implies for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds (( |.z.| " ) * |.(R /. z).|) < r

      proof

        assume

         A2: R is RestFunc-like;

        given r be Real such that

         A3: r > 0 and

         A4: for d be Real st d > 0 holds ex z be Real st z <> 0 & |.z.| < d & not (( |.z.| " ) * |.(R /. z).|) < r;

        defpred P[ Nat, Real] means $2 <> 0 & |.$2.| < (1 / ($1 + 1)) & not ((( |.$2.| " ) * |.(R /. $2).|) < r);



         A5: for n be Element of NAT holds ex z be Element of REAL st P[n, z]

        proof

          let n be Element of NAT ;

          reconsider d = (1 / (n + 1)) as Element of REAL by XREAL_0:def 1;

          d <> 0 by XCMPLX_1: 50;

          then

          consider z be Real such that

           A6: z <> 0 & |.z.| < d & not (( |.z.| " ) * |.(R /. z).|) < r by A4;

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

          take z;

          thus thesis by A6;

        end;

        consider s be Real_Sequence such that

         A7: for n be Element of NAT holds P[n, (s . n)] from FUNCT_2:sch 3( A5);



         A8: for n be Nat holds P[n, (s . n)]

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A7;

        end;

         A9:

        now

          let p be Real;

          assume

           A10: 0 < p;

          consider n be Nat such that

           A11: (p " ) < n by SEQ_4: 3;

          reconsider q0 = 0 , q1 = 1 as Real;

          ((p " ) + q0) < (n + q1) by A11, XREAL_1: 8;

          then

           A12: (1 / (n + 1)) < (1 / (p " )) by A10, XREAL_1: 76;

          take n;

          let m be Nat;



           A13: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A14: (n + 1) <= (m + 1) by XREAL_1: 6;

          (1 / (m + 1)) <= (1 / (n + 1)) by A14, XREAL_1: 118;

          then

           A15: |.((s . m) - 0 ).| < (1 / (n + 1)) by A7, XXREAL_0: 2, A13;

          (1 / (p " )) = p by XCMPLX_1: 216;

          hence |.((s . m) - 0 ).| < p by A12, A15, XXREAL_0: 2;

        end;



         A16: s is convergent by A9, SEQ_2:def 6;

        then ( lim s) = 0 by A9, SEQ_2:def 7;

        then

        reconsider s as non-zero 0 -convergent Real_Sequence by A16, A8, SEQ_1: 5, FDIFF_1:def 1;

        ((s " ) (#) (R /* s)) is convergent & ( lim ((s " ) (#) (R /* s))) = 0 by A2;

        then

        consider n0 be Nat such that

         A17: for m be Nat st n0 <= m holds |.((((s " ) (#) (R /* s)) . m) - 0 ).| < r by A3, SEQ_2:def 7;

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



         A18: |.(((s . n0) " ) * (R /. (s . n0))).| = ( |.((s . n0) " ).| * |.(R /. (s . n0)).|) by COMPLEX1: 65

        .= (( |.(s . n0).| " ) * |.(R /. (s . n0)).|) by COMPLEX1: 66;

        ( dom R) = REAL by A1, PARTFUN1:def 2;

        then

         A19: ( rng s) c= ( dom R);

         |.((((s " ) (#) (R /* s)) . n0) - 0 ).| = |.(((s " ) . n0) * ((R /* s) . n0)).| by SEQ_1: 8

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

        .= |.(((s . n0) " ) * (R /. (s . n0))).| by A19, FUNCT_2: 109;

        hence contradiction by A7, A17, A18;

      end;

      assume

       A20: for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds (( |.z.| " ) * |.(R /. z).|) < r;

      thus R is total by A1;

      let s be non-zero 0 -convergent Real_Sequence;



       A21: s is convergent & ( lim s) = 0 ;

       A22:

      now

        let r be Real;

        assume r > 0 ;

        then

        consider d be Real such that

         A23: d > 0 and

         A24: for z be Real st z <> 0 & |.z.| < d holds (( |.z.| " ) * |.(R /. z).|) < r by A20;

        consider n0 be Nat such that

         A25: for m be Nat st n0 <= m holds |.((s . m) - 0 ).| < d by A21, A23, SEQ_2:def 7;

        take n0;

        thus for m be Nat st n0 <= m holds |.((((s " ) (#) (R /* s)) . m) - 0 ).| < r

        proof

          ( dom R) = REAL by A1, PARTFUN1:def 2;

          then

           A26: ( rng s) c= ( dom R);

          let m be Nat;



           A27: m in NAT by ORDINAL1:def 12;

          assume n0 <= m;

          then

           A28: |.((s . m) - 0 ).| < d by A25;

          (( |.(s . m).| " ) * |.(R /. (s . m)).|) = ( |.((s . m) " ).| * |.(R /. (s . m)).|) by COMPLEX1: 66

          .= |.(((s . m) " ) * (R /. (s . m))).| by COMPLEX1: 65

          .= |.(((s . m) " ) * ((R /* s) . m)).| by A26, FUNCT_2: 109, A27

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

          .= |.((((s " ) (#) (R /* s)) . m) - 0 ).| by SEQ_1: 8;

          hence thesis by A24, A28, SEQ_1: 5;

        end;

      end;

      hence ((s " ) (#) (R /* s)) is convergent by SEQ_2:def 6;

      hence ( lim ((s " ) (#) (R /* s))) = 0 by A22, SEQ_2:def 7;

    end;

    reserve Z for open Subset of REAL ,

y0 for VECTOR of ( REAL-NS n),

G for Function of ( REAL-NS n), ( REAL-NS n);

    theorem :: ORDEQ_01:36



     Th36: for f be continuous PartFunc of REAL , ( REAL-NS n), g be PartFunc of REAL , ( REAL-NS n) st a <= b & ( 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 /. a) = y0 & 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 , ( REAL-NS n), g be PartFunc of REAL , ( REAL-NS n);

      assume

       A1: a <= b & ( 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)));



       A2: f is_integrable_on ['a, b'] by A1, Th33;



       A3: (f | ['a, b']) is bounded by A1, Th32;



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

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

      consider F0 be Function of REAL , ( REAL-NS n) such that

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

      set F = (F0 | ['a, b']);



       A6: ( dom F) = (( dom F0) /\ ['a, b']) by RELAT_1: 61

      .= ( REAL /\ ['a, b']) by FUNCT_2:def 1

      .= ['a, b'] by XBOOLE_1: 28;

       A7:

      now

        let x be Real;

        assume x in [.a, b.];

        then

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



         A9: x in REAL by XREAL_0:def 1;



        thus (F . x) = (F0 . x) by A8, A6, FUNCT_1: 47

        .= ( integral (f,a,x)) by A5, A9;

      end;



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



       A11: for x be Real st x in [.a, b.] holds F is_continuous_in x by Th34, A1, A6, A7;



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



       A13: Z c= ( dom F) by A1, A6, A10, INTEGRA5:def 3;

       A14:

      now

        let x be Real;

        assume

         A15: x in Z;

        then f is_continuous_in x by A10, A4, A1, NFCONT_3:def 2;

        hence F is_differentiable_in x & ( diff (F,x)) = (f /. x) by A15, A1, A2, A3, A12, A13, INTEGR19: 55;

      end;

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

      then

       A16: F is_differentiable_on Z by A13, NDIFF_3: 10;

      set G0 = ( REAL --> y0);

      set G = (G0 | ['a, b']);



       A17: ( dom G) = (( dom G0) /\ ['a, b']) by RELAT_1: 61

      .= ( REAL /\ ['a, b'])

      .= ['a, b'] by XBOOLE_1: 28;

       A18:

      now

        let x be Real;

        assume x in [.a, b.];

        then

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



        thus (G . x) = (G0 . x) by A19, A17, FUNCT_1: 47

        .= y0 by XREAL_0:def 1, FUNCOP_1: 7;

      end;



       A20: F is continuous by A4, A6, A11, NFCONT_3:def 2;



       A21: (G | Z) is constant;

      then

       A22: G is_differentiable_on Z & for x be Real st x in Z holds ((G `| Z) . x) = ( 0. ( REAL-NS n)) by A17, A1, A10, A4, NDIFF_3: 20;



       A23: ( dom g) = (( dom F) /\ ( dom G)) by A6, A17, A1;

      now

        let x be Element of REAL ;

        assume

         A24: x in ( dom g);



         A25: x in [.a, b.] by A24, A1, INTEGRA5:def 3;



         A26: (G /. x) = (G . x) by A24, A1, A17, PARTFUN1:def 6

        .= y0 by A25, A18;



         A27: (F /. x) = (F . x) by A24, A1, A6, PARTFUN1:def 6

        .= ( integral (f,a,x)) by A25, A7;



        thus (g /. x) = (g . x) by A24, PARTFUN1:def 6

        .= ((G /. x) + (F /. x)) by A26, A27, A1, A24;

      end;

      then

       A28: g = (G + F) by A23, VFUNCT_1:def 1;

      thus g is continuous by A20, A28;



       A29: a in ['a, b'] by A1, A4;



       A30: ( 0. ( REAL-NS n)) = (( integral (f,a,a)) - ( integral (f,a,a))) by RLVECT_1: 15

      .= ((( integral (f,a,a)) + ( integral (f,a,a))) - ( integral (f,a,a))) by A29, A1, Th33, A3, INTEGR19: 53

      .= (( integral (f,a,a)) + (( integral (f,a,a)) - ( integral (f,a,a)))) by RLVECT_1: 28

      .= (( integral (f,a,a)) + ( 0. ( REAL-NS n))) by RLVECT_1: 15

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



      thus (g /. a) = (g . a) by A1, A29, PARTFUN1:def 6

      .= (y0 + ( integral (f,a,a))) by A1, A29

      .= y0 by A30;



       A31: g is_differentiable_on Z & for x be Real st x in Z holds ((g `| Z) . x) = (( diff (G,x)) + ( diff (F,x))) by A28, A16, A22, A1, A10, A4, NDIFF_3: 17;

      thus g is_differentiable_on Z by A28, A16, A22, A1, A10, A4, NDIFF_3: 17;

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

      proof

        let t be Real;

        assume

         A32: t in Z;



         A33: ( diff (g,t)) = ((g `| Z) . t) by A31, A32, NDIFF_3:def 6

        .= (( diff (G,t)) + ( diff (F,t))) by A28, A16, A22, A1, A10, A4, NDIFF_3: 17, A32;



         A34: ( diff (G,t)) = ((G `| Z) . t) by A22, A32, NDIFF_3:def 6

        .= ( 0. ( REAL-NS n)) by A21, A17, A1, A10, A4, NDIFF_3: 20, A32;



        thus ( diff (g,t)) = (( 0. ( REAL-NS n)) + (f /. t)) by A33, A34, A14, A32

        .= (f /. t);

      end;

    end;

    theorem :: ORDEQ_01:37

    for i be Nat, y1,y2 be Point of ( REAL-NS n) holds (( proj (i,n)) . (y1 + y2)) = ((( proj (i,n)) . y1) + (( proj (i,n)) . y2))

    proof

      let i be Nat, y1,y2 be Point of ( REAL-NS n);

      reconsider yy1 = y1, yy2 = y2 as Element of ( REAL n) by REAL_NS1:def 4;

      reconsider ry1 = (yy1 . i) as Real;

      reconsider ry2 = (yy2 . i) as Real;



       A1: (( proj (i,n)) . y1) = ry1 & (( proj (i,n)) . y2) = ry2 by PDIFF_1:def 1;

      (( proj (i,n)) . (y1 + y2)) = (( proj (i,n)) . (yy1 + yy2)) by REAL_NS1: 2

      .= ((yy1 + yy2) . i) by PDIFF_1:def 1

      .= (ry1 + ry2) by RVSUM_1: 11;

      hence thesis by A1;

    end;

    theorem :: ORDEQ_01:38



     Th38: for i be Nat, y1 be Point of ( REAL-NS n), r be Real holds (( proj (i,n)) . (r * y1)) = (r * (( proj (i,n)) . y1))

    proof

      let i be Nat, y1 be Point of ( REAL-NS n), r be Real;

      reconsider yy1 = y1 as Element of ( REAL n) by REAL_NS1:def 4;

      reconsider y1i = (yy1 . i) as Element of REAL by XREAL_0:def 1;

      (( proj (i,n)) . (r * y1)) = (( proj (i,n)) . (r * yy1)) by REAL_NS1: 3

      .= ((r * yy1) . i) by PDIFF_1:def 1

      .= (r * y1i) by RVSUM_1: 44;

      hence thesis by PDIFF_1:def 1;

    end;

    theorem :: ORDEQ_01:39



     Th39: for g be PartFunc of REAL , ( REAL-NS n), x0 be Real, i be Nat st 1 <= i & i <= n & g is_differentiable_in x0 holds (( proj (i,n)) * g) is_differentiable_in x0 & (( proj (i,n)) . ( diff (g,x0))) = ( diff ((( proj (i,n)) * g),x0))

    proof

      let g be PartFunc of REAL , ( REAL-NS n), x0 be Real, i be Nat;

      assume

       A1: 1 <= i & i <= n & g is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A2: N c= ( dom g) & ex DFG be LinearFunc of ( REAL-NS n), GR be RestFunc of ( REAL-NS n) st ( diff (g,x0)) = (DFG /. 1) & for x be Real st x in N holds ((g /. x) - (g /. x0)) = ((DFG /. (x - x0)) + (GR /. (x - x0))) by NDIFF_3:def 4;

      consider DFG be LinearFunc of ( REAL-NS n), GR be RestFunc of ( REAL-NS n) such that

       A3: ( diff (g,x0)) = (DFG /. 1) & for x be Real st x in N holds ((g /. x) - (g /. x0)) = ((DFG /. (x - x0)) + (GR /. (x - x0))) by A2;

      consider LP be Point of ( REAL-NS n) such that

       A4: for p be Real holds (DFG /. p) = (p * LP) by NDIFF_3:def 2;



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

      then

      reconsider PG = ( proj (i,n)) as Function of ( REAL-NS n), REAL ;

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

      then

      reconsider L = (( proj (i,n)) * DFG) as Function of REAL , REAL ;



       A6: for r be Real holds (L . r) = ((( proj (i,n)) . LP) * r)

      proof

        let r be Real;



         A7: ( dom L) = REAL by FUNCT_2:def 1;

        ( dom DFG) = REAL by FUNCT_2:def 1;



        then (DFG . r) = (DFG /. r) by XREAL_0:def 1, PARTFUN1:def 6

        .= (r * LP) by A4;

        then (( proj (i,n)) . (DFG . r)) = (r * (( proj (i,n)) . LP)) by Th38;

        hence (L . r) = ((( proj (i,n)) . LP) * r) by A7, FUNCT_1: 12, XREAL_0:def 1;

      end;

      reconsider L as LinearFunc by A6, FDIFF_1:def 3;



       A8: GR is total by NDIFF_3:def 1;

      then

      reconsider FGR = GR as Function of REAL , ( REAL-NS n);



       A9: (( proj (i,n)) * FGR) is Function of REAL , REAL by A5;

      (( proj (i,n)) * GR) is RestFunc

      proof



         A10: ( dom GR) = REAL by A8, PARTFUN1:def 2;

        reconsider R = (( proj (i,n)) * GR) as PartFunc of REAL , REAL ;

        for r be Real st r > 0 holds ex d be Real st d > 0 & (for z be Real st z <> 0 & |.z.| < d holds (( |.z.| " ) * |.(R /. z).|) < r)

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider d be Real such that

           A11: d > 0 & (for z be Real st z <> 0 & |.z.| < d holds (( |.z.| " ) * ||.(GR /. z).||) < r) by A8, NDIFF_4: 23;

          take d;

          thus d > 0 by A11;

          let z be Real;

          assume

           A12: z <> 0 & |.z.| < d;



           A13: z in REAL by XREAL_0:def 1;



           A14: (GR /. z) = (GR . z) by A10, PARTFUN1:def 6, XREAL_0:def 1;



           A15: i in ( Seg n) by A1;

          reconsider GRz = (GR /. z) as Point of ( REAL-NS n);

          reconsider GRz1 = GRz as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider GRzi = (GRz1 . i) as Real;

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

          then ( dom ( proj (i,n))) = the carrier of ( REAL-NS n) by PARTFUN1:def 2;

          then

           A16: z in ( dom (( proj (i,n)) * GR)) by A10, A14, FUNCT_1: 11, A13;



          then

           A17: ((( proj (i,n)) * GR) . z) = (( proj (i,n)) . (GR . z)) by FUNCT_1: 12

          .= (( proj (i,n)) . GRz1) by A10, A13, PARTFUN1:def 6;



           A18: |.GRzi.| <= ||.(GR /. z).|| by A15, REAL_NS1: 9;



           A19: 0 <= |.z.| by COMPLEX1: 46;

           0 <= |.GRzi.| by COMPLEX1: 46;

          then

           A20: (( |.z.| " ) * |.GRzi.|) <= (( |.z.| " ) * ||.(GR /. z).||) by A18, A19, XREAL_1: 66;

          (( |.z.| " ) * ||.(GR /. z).||) < r by A11, A12;

          then

           A21: (( |.z.| " ) * |.GRzi.|) < r by A20, XXREAL_0: 2;

          reconsider Rz = ((( proj (i,n)) * GR) . z) as Element of REAL by XREAL_0:def 1;

          (( |.z.| " ) * |.Rz.|) < r by A21, PDIFF_1:def 1, A17;

          hence thesis by A16, PARTFUN1:def 6;

        end;

        hence thesis by A9, Th35;

      end;

      then

      reconsider R = (( proj (i,n)) * GR) as RestFunc;

      set pg = (( proj (i,n)) * g);

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

      then ( dom ( proj (i,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

      then ( rng g) c= ( dom ( proj (i,n)));

      then

       A22: ( dom g) = ( dom (( proj (i,n)) * g)) by RELAT_1: 27;



       A23: for x be Real st x in N holds ((pg . x) - (pg . x0)) = ((L . (x - x0)) + (R . (x - x0)))

      proof

        let x be Real;

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

        now

          assume

           A24: x in N;

          then

           A25: ((g /. x) - (g /. x0)) = ((DFG /. (xx - x0)) + (GR /. (xx - x0))) by A3;



           A26: x0 in N by RCOMP_1: 16;



           A27: (g /. x) = (g . x) & (g /. x0) = (g . x0) by A2, A24, A26, PARTFUN1:def 6;

          reconsider PGSx = ((pg . x) - (pg . x0)) as Element of REAL by XREAL_0:def 1;

          reconsider PGdx = (pg . x) as Element of REAL by XREAL_0:def 1;

          reconsider PGdx0 = (pg . x0) as Element of REAL by XREAL_0:def 1;

          (g . x) in ( rng g) by A2, A24, FUNCT_1: 3;

          then

          reconsider Gx = (g . x) as Element of ( REAL n) by REAL_NS1:def 4;

          (g . x0) in ( rng g) by A2, A26, FUNCT_1: 3;

          then

          reconsider Gx0 = (g . x0) as Element of ( REAL n) by REAL_NS1:def 4;

          set projGx = (( proj (i,n)) . (g . x));

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

          set projGx0 = (( proj (i,n)) . (g . x0));

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

          reconsider Gx1 = Gx as Element of ( REAL-NS n) by REAL_NS1:def 4;

          reconsider Gx01 = Gx0 as Element of ( REAL-NS n) by REAL_NS1:def 4;

          reconsider Gsx = (g /. x) as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider Gsx0 = (g /. x0) as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider dxx0 = (x - x0) as Element of REAL by XREAL_0:def 1;

          reconsider Ldxx0 = (L . (x - x0)) as Element of REAL by XREAL_0:def 1;



           A28: ( dom R) = REAL by A9, PARTFUN1:def 2;

          reconsider Rdxx0 = (R . (x - x0)) as Element of REAL by XREAL_0:def 1;

          reconsider Lxx0Rxx0 = ((L . (x - x0)) + (R . (x - x0))) as Element of REAL by XREAL_0:def 1;

          reconsider Ldiff = (DFG /. (x - x0)) as Element of ( REAL n) by REAL_NS1:def 4;

          set projLdiff = (( proj (i,n)) . Ldiff);

          reconsider projLdiff as Element of REAL ;



           A29: ( dom GR) = REAL by A8, PARTFUN1:def 2;

          then (GR . dxx0) in ( rng GR) by FUNCT_1: 3;

          then

          reconsider Rdiff = (GR . dxx0) as Element of ( REAL n) by REAL_NS1:def 4;

          set projRdiff = (( proj (i,n)) . Rdiff);

          reconsider projRdiff as Element of REAL ;

          ( dom DFG) = REAL by FUNCT_2:def 1;

          then

           A30: Ldiff = (DFG . (x - x0)) by PARTFUN1:def 6, XREAL_0:def 1;

          ( dom L) = REAL by FUNCT_2:def 1;

          then

           A31: (L . (x - x0)) = (( proj (i,n)) . Ldiff) by FUNCT_1: 12, XREAL_0:def 1, A30;



           A32: (R . (x - x0)) = (( proj (i,n)) . Rdiff) by A28, FUNCT_1: 12;



           A33: (( proj (i,n)) . Ldiff) = (Ldiff . i) by PDIFF_1:def 1;



           A34: (( proj (i,n)) . Rdiff) = (Rdiff . i) by PDIFF_1:def 1;

          reconsider diffGR = ((DFG /. (x - x0)) + (GR /. (x - x0))) as Element of ( REAL n) by REAL_NS1:def 4;

          reconsider Rsdiff = (GR /. (x - x0)) as Element of ( REAL n) by REAL_NS1:def 4;

          PGSx = (projGx - PGdx0) by A2, A22, A24, FUNCT_1: 12

          .= ((( proj (i,n)) . Gx1) - (( proj (i,n)) . Gx01)) by A2, A22, A26, FUNCT_1: 12

          .= ((Gx . i) - (( proj (i,n)) . Gx01)) by PDIFF_1:def 1

          .= ((Gx . i) - (Gx0 . i)) by PDIFF_1:def 1

          .= ((Gsx - Gsx0) . i) by A27, RVSUM_1: 27

          .= (diffGR . i) by A25, REAL_NS1: 5

          .= ((Ldiff + Rsdiff) . i) by REAL_NS1: 2

          .= ((Ldiff . i) + (Rsdiff . i)) by RVSUM_1: 11;

          hence thesis by A31, A33, A34, A29, PARTFUN1:def 6, A32;

        end;

        hence thesis;

      end;

      hence

       A35: (( proj (i,n)) * g) is_differentiable_in x0 by A2, A22;

      (L . 1) = (1 * (( proj (i,n)) . LP)) by A6

      .= (( proj (i,n)) . (1 qua Real * LP)) by RLVECT_1:def 8

      .= (( proj (i,n)) . ( diff (g,x0))) by A3, A4;

      hence (( proj (i,n)) . ( diff (g,x0))) = ( diff ((( proj (i,n)) * g),x0)) by A35, A2, A22, A23, FDIFF_1:def 5;

    end;



     Lm7: for i be Nat holds (( proj (i,n)) . ( 0. ( REAL-NS n))) = 0

    proof

      let i be Nat;



      thus (( proj (i,n)) . ( 0. ( REAL-NS n))) = (( proj (i,n)) . ( 0* n)) by REAL_NS1:def 4

      .= (( 0* n) . i) by PDIFF_1:def 1

      .= 0 ;

    end;

    theorem :: ORDEQ_01:40



     Th40: for f be PartFunc of REAL , ( REAL-NS n), X be set st for i be Nat st 1 <= i & i <= n holds ((( proj (i,n)) * f) | X) is constant holds (f | X) is constant

    proof

      let f be PartFunc of REAL , ( REAL-NS n), X be set;

      assume

       A1: for i be Nat st 1 <= i & i <= n holds ((( proj (i,n)) * f) | X) is constant;



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

      now

        let x,y be object;

        assume

         A3: x in ( dom (f | X)) & y in ( dom (f | X));

        then

         A4: x in ( dom f) & x in X & y in ( dom f) & y in X by RELAT_1: 57;

        (f . x) in ( rng f) by A4, FUNCT_1: 3;

        then

        reconsider fx = (f . x) as Element of ( REAL n) by REAL_NS1:def 4;

        (f . y) in ( rng f) by A4, FUNCT_1: 3;

        then

        reconsider fy = (f . y) as Element of ( REAL n) by REAL_NS1:def 4;



         A5: ( len fy) = n by CARD_1:def 7;



         A6: ( len fx) = n by CARD_1:def 7;

        now

          let i be Nat;

          assume

           A7: 1 <= i & i <= ( len fx);

          ( dom ( proj (i,n))) = the carrier of ( REAL-NS n) by A2, FUNCT_2:def 1;

          then ( rng f) c= ( dom ( proj (i,n)));

          then

           A8: ( dom f) = ( dom (( proj (i,n)) * f)) by RELAT_1: 27;



           A9: (((( proj (i,n)) * f) | X) . x) = ((( proj (i,n)) * f) . x) by A3, FUNCT_1: 49

          .= (( proj (i,n)) . (f . x)) by A4, FUNCT_1: 13

          .= (fx . i) by PDIFF_1:def 1;



           A10: (((( proj (i,n)) * f) | X) . y) = ((( proj (i,n)) * f) . y) by A3, FUNCT_1: 49

          .= (( proj (i,n)) . (f . y)) by A4, FUNCT_1: 13

          .= (fy . i) by PDIFF_1:def 1;



           A11: ((( proj (i,n)) * f) | X) is constant by A1, A7, A6;

          x in ( dom ((( proj (i,n)) * f) | X)) & y in ( dom ((( proj (i,n)) * f) | X)) by A8, A4, RELAT_1: 57;

          hence (fx . i) = (fy . i) by A9, A10, A11, FUNCT_1:def 10;

        end;

        then

         A12: fx = fy by A5, CARD_1:def 7;



        thus ((f | X) . x) = (f . x) by A3, FUNCT_1: 49

        .= ((f | X) . y) by A3, A12, FUNCT_1: 49;

      end;

      hence thesis by FUNCT_1:def 10;

    end;

    theorem :: ORDEQ_01:41



     Th41: for f be PartFunc of REAL , ( REAL-NS n) st ].a, b.[ c= ( dom f) & f is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (f,x)) = ( 0. ( REAL-NS n)) holds (f | ].a, b.[) is constant

    proof

      let f be PartFunc of REAL , ( REAL-NS n);

      assume

       A1: ].a, b.[ c= ( dom f) & f is_differentiable_on ].a, b.[ & for x be Real st x in ].a, b.[ holds ( diff (f,x)) = ( 0. ( REAL-NS n));

      reconsider Z = ].a, b.[ as open Subset of REAL ;

      now

        let i be Nat;

        assume

         A2: 1 <= i & i <= n;

         A3:

        now

          let x be Real;

          assume x in Z;

          then f is_differentiable_in x by A1, NDIFF_3: 10;

          hence (( proj (i,n)) * f) is_differentiable_in x & (( proj (i,n)) . ( diff (f,x))) = ( diff ((( proj (i,n)) * f),x)) by A2, Th39;

        end;



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

        ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

        then ( rng f) c= ( dom ( proj (i,n))) by A4;

        then

         A5: Z c= ( dom (( proj (i,n)) * f)) by A1, RELAT_1: 27;

        for x be Real st x in Z holds (( proj (i,n)) * f) is_differentiable_in x by A3;

        then

         A6: (( proj (i,n)) * f) is_differentiable_on ].a, b.[ by A5, FDIFF_1: 9;

        for x be Real st x in ].a, b.[ holds ( diff ((( proj (i,n)) * f),x)) = 0

        proof

          let x be Real;

          assume

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

          then

           A8: (( proj (i,n)) . ( diff (f,x))) = ( diff ((( proj (i,n)) * f),x)) by A3;

          ( diff (f,x)) = ( 0. ( REAL-NS n)) by A1, A7;

          hence ( diff ((( proj (i,n)) * f),x)) = 0 by Lm7, A8;

        end;

        hence ((( proj (i,n)) * f) | ].a, b.[) is constant by A6, ROLLE: 7;

      end;

      hence thesis by Th40;

    end;

    theorem :: ORDEQ_01:42



     Th42: for f be continuous PartFunc of REAL , ( REAL-NS n) st a < b & [.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 , ( REAL-NS n);

      assume

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



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

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



       A3: 0 < (b - a) by A1, 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 A1, 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 ( REAL-NS n);



       A6: ( dom (f | ].a, b.[)) = (( dom f) /\ ].a, b.[) by RELAT_1: 61

      .= ].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;



       A10: a in ( dom f) by A1;



       A11: b in ( dom f) by A1;

      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);



       A14: f is_continuous_in a by A10, NFCONT_3:def 2;

       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;



         A18: 0 < (d / (x + 1)) by A4, XREAL_1: 139;

        (1 + 0 qua Real) <= (1 + x) by XREAL_1: 7;

        then

         A19: (d / (x + 1)) <= (d / 1) by XREAL_1: 118, A3;



         A20: (a + 0 qua Real) < (a + (d / (x + 1))) by A18, XREAL_1: 8;

        (a + (d / (x + 1))) <= (a + d) by A19, 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.[ by TARSKI:def 3;

      then

       A22: ( rng s1) c= ( dom f) by A2, A1, XBOOLE_1: 1;

       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

         A26: d < ((n + 1) * p) by A24, XCMPLX_1: 87;



         A27: (d / (n + 1)) < p by A26, XREAL_1: 83;



         A28: |.(d / (n + 1)).| = (d / (n + 1)) by A3, ABSVALUE:def 1;



         A29: |.(d / (n + 1)).| < p by A27, A3, ABSVALUE:def 1;

        take n;

        thus for m be Nat st n <= m holds |.((s1 . m) - a).| < p

        proof

          let m be Nat;



           A30: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A31: (n + 1) <= (m + 1) by XREAL_1: 7;

          (d / (m + 1)) <= (d / (n + 1)) by A3, A31, XREAL_1: 118;

          then

           A32: |.(d / (m + 1)).| <= |.(d / (n + 1)).| by A28, A3, ABSVALUE:def 1;

           |.((s1 . m) - a).| = |.((a + (d / (m + 1))) - a).| by A13, A30

          .= |.(d / (m + 1)).|;

          hence |.((s1 . m) - a).| < p by A32, A29, XXREAL_0: 2;

        end;

      end;

      then

       A33: s1 is convergent by SEQ_2:def 6;

      then

       A34: ( lim s1) = a by A23, SEQ_2:def 7;



       A35: (f /* s1) is convergent & (f /. a) = ( lim (f /* s1)) by A14, A22, A33, A34, NFCONT_3:def 1;



       A36: for i be Nat holds ((f /* s1) . i) = f0

      proof

        let i be Nat;



         A37: i in NAT by ORDINAL1:def 12;

        then

         A38: (s1 . i) in ( rng s1) by FUNCT_2: 4;



        thus ((f /* s1) . i) = (f /. (s1 . i)) by A21, FUNCT_2: 109, XBOOLE_1: 1, A1, A2, A37

        .= f0 by A7, A38, A15;

      end;

      now

        let r be Real;

        assume

         A39: 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 A36

          .= ||.( 0. ( REAL-NS n)).|| by RLVECT_1: 15

          .= 0 ;

          hence thesis by A39;

        end;

      end;

      then ( lim (f /* s1)) = f0 by A35, NORMSP_1:def 7;

      then

       A40: (f . a) = f0 by A35, A10, PARTFUN1:def 6;

      deffunc F2( Nat) = (b - (d / ($1 + 1)));



       A41: 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

       A42: for x be Element of NAT holds (s2 . x) = F2(x) from FUNCT_2:sch 9( A41);



       A43: f is_continuous_in b by A11, NFCONT_3:def 2;

       A44:

      now

        let y be object;

        assume y in ( rng s2);

        then

        consider x be object such that

         A45: x in ( dom s2) & y = (s2 . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A45;



         A46: y = (b - (d / (x + 1))) by A42, A45;



         A47: 0 < (d / (x + 1)) by A4, XREAL_1: 139;

        (1 + 0 qua Real) <= (1 + x) by XREAL_1: 7;

        then

         A48: (d / (x + 1)) <= (d / 1) by XREAL_1: 118, A3;



         A49: (b - (d / (x + 1))) < (b - 0 qua Real) by A47, XREAL_1: 15;

        (b - d) <= (b - (d / (x + 1))) by A48, XREAL_1: 13;

        then a < (b - (d / (x + 1))) by A5, XXREAL_0: 2;

        hence y in ].a, b.[ by A46, A49;

      end;

      then

       A50: ( rng s2) c= ].a, b.[ by TARSKI:def 3;

      then

       A51: ( rng s2) c= ( dom f) by A2, A1, XBOOLE_1: 1;

       A52:

      now

        let p be Real;

        assume

         A53: 0 < p;

        consider n be Nat such that

         A54: (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, A54;

        then ((d / p) * p) < ((n + 1) * p) by A53, XREAL_1: 68;

        then

         A55: d < ((n + 1) * p) by A53, XCMPLX_1: 87;



         A56: (d / (n + 1)) < p by A55, XREAL_1: 83;

        take n;

        thus for m be Nat st n <= m holds |.((s2 . m) - b).| < p

        proof

          let m be Nat;



           A57: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A58: (n + 1) <= (m + 1) by XREAL_1: 7;



           A59: (d / (m + 1)) <= (d / (n + 1)) by A3, A58, XREAL_1: 118;



           A60: |.(d / (m + 1)).| = (d / (m + 1)) by A3, ABSVALUE:def 1;

           |.((s2 . m) - b).| = |.((b - (d / (m + 1))) - b).| by A42, A57

          .= |.( - (d / (m + 1))).|

          .= |.(d / (m + 1)).| by COMPLEX1: 52;

          hence |.((s2 . m) - b).| < p by A60, XXREAL_0: 2, A59, A56;

        end;

      end;

      then

       A61: s2 is convergent by SEQ_2:def 6;

      then

       A62: ( lim s2) = b by A52, SEQ_2:def 7;



       A63: (f /* s2) is convergent & (f /. b) = ( lim (f /* s2)) by A43, A51, A61, A62, NFCONT_3:def 1;



       A64: for i be Element of NAT holds ((f /* s2) . i) = f0

      proof

        let i be Element of NAT ;



         A65: (s2 . i) in ( rng s2) by FUNCT_2: 4;



        thus ((f /* s2) . i) = (f /. (s2 . i)) by A2, A1, XBOOLE_1: 1, A50, FUNCT_2: 109

        .= f0 by A7, A65, A44;

      end;

      now

        let r be Real;

        assume

         A66: 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 A64

          .= ||.( 0. ( REAL-NS n)).|| by RLVECT_1: 15

          .= 0 ;

          hence thesis by A66;

        end;

      end;

      then ( lim (f /* s2)) = f0 by A63, NORMSP_1:def 7;

      then

       A67: (f . b) = f0 by A63, A11, PARTFUN1:def 6;

      let x be Real;

      assume x in [.a, b.];

      then

       A68: ex r be Real st x = r & a <= r & r <= b;

      per cases ;

        suppose

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



        hence (f . x) = (f /. x) by A1, A2, PARTFUN1:def 6

        .= (f . a) by A40, A69, A7;

      end;

        suppose not x in ].a, b.[;

        then x <= a or b <= x;

        hence (f . x) = (f . a) by A40, A67, A68, XXREAL_0: 1;

      end;

    end;

    theorem :: ORDEQ_01:43



     Th43: for y,Gf be continuous PartFunc of REAL , ( REAL-NS n), g be PartFunc of REAL , ( REAL-NS n) 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 , ( REAL-NS n), g be PartFunc of REAL , ( REAL-NS n);

      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 Th36;



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



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

      reconsider h = (y - g) as continuous PartFunc of REAL , ( REAL-NS n) by A2;



       A5: ( dom h) = ( ['a, b'] /\ ['a, b']) by A1, VFUNCT_1:def 2

      .= ['a, b'];

      then

       A6: ].a, b.[ c= ( dom h) by A3, XXREAL_1: 25;



       A7: h is_differentiable_on ].a, b.[ by A1, A2, NDIFF_3: 18, A4, A3, A5;

       A8:

      now

        let x be Real;

        assume

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

        then

         A10: ( diff (y,x)) = (Gf /. x) by A1;



         A11: ( diff (g,x)) = (Gf /. x) by A1, A9, Th36;



        thus ( diff (h,x)) = (((y - g) `| ].a, b.[) . x) by A9, A7, NDIFF_3:def 6

        .= ((Gf /. x) - (Gf /. x)) by A10, A11, A1, A2, A6, A9, NDIFF_3: 18

        .= ( 0. ( REAL-NS n)) by RLVECT_1: 15;

      end;



       A12: (h | ].a, b.[) is constant by Th41, A5, A7, A8, A3, XXREAL_1: 25;



       A13: for x be Real st x in ( dom h) holds (h . x) = ( 0. ( REAL-NS n))

      proof

        let x be Real;

        assume

         A14: x in ( dom h);



         A15: a in ( dom h) by A5, A1, A3;



        thus (h . x) = (h . a) by A14, Th42, A1, A12, A3, A5

        .= (h /. a) by A15, PARTFUN1:def 6

        .= (y0 - y0) by A2, A1, A15, VFUNCT_1:def 2

        .= ( 0. ( REAL-NS n)) 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. ( REAL-NS n)) = (h . x) by A13, A1, A5

        .= (h /. x) by A16, A1, A5, PARTFUN1:def 6

        .= ((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) = (g /. x) by A17, A16, PARTFUN1:def 6

        .= (g . x) by A16, A1, PARTFUN1:def 6;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: ORDEQ_01:44



     Th44: for a,b,c,d be Real, f be PartFunc of REAL , ( REAL-NS n) st a <= b & f is_integrable_on ['a, b'] & ||.f.|| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'] holds ||.f.|| is_integrable_on ['( min (c,d)), ( max (c,d))'] & ( ||.f.|| | ['( min (c,d)), ( max (c,d))']) is bounded & ||.( integral (f,c,d)).|| <= ( integral ( ||.f.||,( min (c,d)),( max (c,d))))

    proof

      let a,b,c,d be Real, f be PartFunc of REAL , ( REAL-NS n);

      assume

       A1: a <= b & f is_integrable_on ['a, b'] & ||.f.|| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['a, b'] c= ( dom f) & c in ['a, b'] & d in ['a, b'];

      reconsider f1 = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;



       A2: (f1 | ['a, b']) is bounded by A1, INTEGR19: 34;



       A3: f1 is_integrable_on ['a, b'] by A2, A1, INTEGR19: 43;



       A4: ||.f.|| = |.f1.| by NFCONT_4: 9;



       A5: |.f1.| is_integrable_on ['a, b'] by A1, NFCONT_4: 9;

       |.f1.| is_integrable_on ['( min (c,d)), ( max (c,d))'] & ( |.f1.| | ['( min (c,d)), ( max (c,d))']) is bounded & |.( integral (f1,c,d)).| <= ( integral ( |.f1.|,( min (c,d)),( max (c,d)))) by A1, A2, A3, A5, INTEGR19: 22;

      hence thesis by A4, REAL_NS1: 1, A1, INTEGR19: 48;

    end;

    theorem :: ORDEQ_01:45



     Th45: for a,b,c,d,e be Real, f be PartFunc of REAL , ( REAL-NS n) st (a <= b & c <= d & f is_integrable_on ['a, b'] & ||.f.|| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['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)) & ||.( integral (f,d,c)).|| <= (e * (d - c))

    proof

      let a,b,c,d,e be Real, f be PartFunc of REAL , ( REAL-NS n);

      assume

       A1: a <= b & c <= d & f is_integrable_on ['a, b'] & ||.f.|| is_integrable_on ['a, b'] & (f | ['a, b']) is bounded & ['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;



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

      then

       A3: ex g be Real st c = g & a <= g & g <= b by A1;



       A4: ex g be Real st d = g & a <= g & g <= b by A2, A1;

      reconsider f1 = f as PartFunc of REAL , ( REAL n) by REAL_NS1:def 4;



       A5: (f1 | ['a, b']) is bounded by A1, INTEGR19: 34;



       A6: f1 is_integrable_on ['a, b'] by A5, A1, INTEGR19: 43;



       A7: |.f1.| is_integrable_on ['a, b'] by A1, NFCONT_4: 9;

      now

        let x be Real;

        assume

         A8: x in ['c, d'];

        then

         A9: ||.(f /. x).|| <= e by A1;



         A10: ['c, d'] c= ( dom f) by A1, INTEGR19: 2, A3, A4;



        then (f /. x) = (f . x) by A8, PARTFUN1:def 6

        .= (f1 /. x) by A8, A10, PARTFUN1:def 6;

        hence |.(f1 /. x).| <= e by A9, REAL_NS1: 1;

      end;

      then |.( integral (f1,c,d)).| <= (e * (d - c)) & |.( integral (f1,d,c)).| <= (e * (d - c)) by A1, A5, A6, A7, INTEGR19: 24;

      hence ||.( integral (f,c,d)).|| <= (e * (d - c)) & ||.( integral (f,d,c)).|| <= (e * (d - c)) by REAL_NS1: 1, A1, INTEGR19: 48;

    end;



     Lm8: for g be Function of REAL , REAL st for x be Real holds (g . x) = (x - a) holds for x be Real holds g is_differentiable_in x & ( diff (g,x)) = 1

    proof

      let g be Function of REAL , REAL ;



       A1: ( dom g) = ( [#] REAL ) by FUNCT_2:def 1;

      assume

       A2: for x be Real holds (g . x) = (x - a);



       A3: for d be Real st d in ( [#] REAL ) holds (g . d) = ((1 * d) + ( - (1 * a)))

      proof

        let d be Real such that d in ( [#] REAL );



        thus (g . d) = (d - a) by A2

        .= ((1 * d) + ( - (1 * a)));

      end;

      then

       A4: g is_differentiable_on ( dom g) by A1, FDIFF_1: 23;

      for x be Real holds g is_differentiable_in x & ( diff (g,x)) = 1

      proof

        let d be Real;

        thus g is_differentiable_in d by A1, A4, XREAL_0:def 1;

        d in REAL by XREAL_0:def 1;



        hence ( diff (g,d)) = ((g `| ( dom g)) . d) by A1, A4, FDIFF_1:def 7

        .= 1 by A1, A3, FDIFF_1: 23, XREAL_0:def 1;

      end;

      hence thesis;

    end;

    theorem :: ORDEQ_01:46



     Th46: for n be Nat, g be Function of REAL , REAL st for x be Real holds (g . x) = ((x - a) |^ (n + 1)) holds for x be Real holds g is_differentiable_in x & ( diff (g,x)) = ((n + 1) * ((x - a) |^ n))

    proof

      let n be Nat;

      let g be Function of REAL , REAL ;



       A1: ( dom g) = REAL by FUNCT_2:def 1;

      assume

       A2: for x be Real holds (g . x) = ((x - a) |^ (n + 1));

      defpred X[ set] means $1 in REAL ;

      deffunc U( Real) = ( In (($1 - a), REAL ));

      consider f be PartFunc of REAL , REAL such that

       A3: for d be Element of REAL holds d in ( dom f) iff X[d] and

       A4: for d be Element of REAL st d in ( dom f) holds (f /. d) = U(d) from PARTFUN2:sch 2;

      for x be object st x in REAL holds x in ( dom f) by A3;

      then REAL c= ( dom f) by TARSKI:def 3;

      then

       A5: ( dom f) = REAL by XBOOLE_0:def 10;



       A6: for d be Element of REAL holds (f . d) = (d - a)

      proof

        let d be Element of REAL ;

        (f /. d) = ( In ((d - a), REAL )) by A4, A5;

        hence thesis by A5, PARTFUN1:def 6;

      end;



       A7: for d be Real holds (f . d) = (d - a)

      proof

        let d be Real;

        d in REAL by XREAL_0:def 1;

        hence thesis by A6;

      end;

      reconsider n1 = (n + 1) as Element of NAT by ORDINAL1:def 12;



       A8: f is Function of REAL , REAL by A5, FUNCT_2: 67;



       A9: ( dom ( #Z n1)) = REAL & ( rng f) c= REAL by FUNCT_2:def 1;

      then

       A10: ( dom (( #Z n1) * f)) = ( dom f) by RELAT_1: 27;

       A11:

      now

        let x be Element of REAL ;

        assume x in ( dom (( #Z n1) * f));



        hence ((( #Z n1) * f) . x) = ((( #Z n1) * f) /. x) by PARTFUN1:def 6

        .= (( #Z n1) /. (f /. x)) by A5, A10, PARTFUN2: 3

        .= (( #Z n1) . (f . x)) by A5, PARTFUN1:def 6

        .= ((f . x) #Z n1) by TAYLOR_1:def 1

        .= ((f . x) |^ (n + 1)) by PREPOWER: 36

        .= ((x - a) |^ (n + 1)) by A6

        .= (g . x) by A2;

      end;

      reconsider n1 = (n + 1), nn = n, n0 = ((n + 1) - 1) as Element of NAT by ORDINAL1:def 12;



       A12: for x be Real holds (( #Z n1) * f) is_differentiable_in x & ( diff ((( #Z n1) * f),x)) = ((n + 1) * ((x - a) |^ n))

      proof

        let x be Real;



         A13: f is_differentiable_in x & ( #Z n1) is_differentiable_in (f . x) by A8, Lm8, A7, TAYLOR_1: 2;

        hence (( #Z n1) * f) is_differentiable_in x by FDIFF_2: 13;

        reconsider pp = ((f . x) #Z n0) as Real;

        reconsider px = ((x - a) #Z nn) as Real;

        ( diff (( #Z n1),(f . x))) = (n1 * pp) by TAYLOR_1: 2;



        hence ( diff ((( #Z n1) * f),x)) = ((n1 * pp) * ( diff (f,x))) by A13, FDIFF_2: 13

        .= ((n1 * pp) * 1) by A8, Lm8, A7

        .= (n1 * px) by A7

        .= ((n + 1) * ((x - a) |^ n)) by PREPOWER: 36;

      end;

      (( #Z n1) * f) = g by A11, PARTFUN1: 5, A1, A5, A9, RELAT_1: 27;

      hence thesis by A12;

    end;

    theorem :: ORDEQ_01:47



     Th47: for n be Nat, g be Function of REAL , REAL st for x be Real holds (g . x) = (((x - a) |^ (n + 1)) / ((n + 1) ! )) holds for x be Real holds g is_differentiable_in x & ( diff (g,x)) = (((x - a) |^ n) / (n ! ))

    proof

      let n be Nat;

      let g be Function of REAL , REAL ;



       A1: ( dom g) = REAL by FUNCT_2:def 1;

      assume

       A2: for x be Real holds (g . x) = (((x - a) |^ (n + 1)) / ((n + 1) ! ));

      defpred X[ set] means $1 in REAL ;

      deffunc U( Real) = ( In ((($1 - a) |^ (n + 1)), REAL ));

      consider f be PartFunc of REAL , REAL such that

       A3: for d be Element of REAL holds d in ( dom f) iff X[d] and

       A4: for d be Element of REAL st d in ( dom f) holds (f /. d) = U(d) from PARTFUN2:sch 2;

      for x be object st x in REAL holds x in ( dom f) by A3;

      then REAL c= ( dom f) by TARSKI:def 3;

      then

       A5: ( dom f) = REAL by XBOOLE_0:def 10;



       A6: for d be Real holds (f . d) = ((d - a) |^ (n + 1))

      proof

        let d be Real;



         A7: d in REAL by XREAL_0:def 1;

        (f /. d) = ( In (((d - a) |^ (n + 1)), REAL )) by A4, A5, A7;

        hence thesis by A5, PARTFUN1:def 6, A7;

      end;



       A8: f is Function of REAL , REAL by A5, FUNCT_2: 67;



       A9: ( dom ((1 / ((n + 1) ! )) (#) f)) = ( dom f) by VALUED_1:def 5;

       A10:

      now

        let x be Element of REAL ;

        assume x in ( dom ((1 / ((n + 1) ! )) (#) f));



        hence (((1 / ((n + 1) ! )) (#) f) . x) = ((1 / ((n + 1) ! )) * (f . x)) by VALUED_1:def 5

        .= ((1 / ((n + 1) ! )) * ((x - a) |^ (n + 1))) by A6

        .= ((((x - a) |^ (n + 1)) / ((n + 1) ! )) * 1) by XCMPLX_1: 75

        .= (g . x) by A2;

      end;



       A11: for x be Real holds ((1 / ((n + 1) ! )) (#) f) is_differentiable_in x & ( diff (((1 / ((n + 1) ! )) (#) f),x)) = (((x - a) |^ n) / (n ! ))

      proof

        let x be Real;



         A12: ((n + 1) / ((n + 1) ! )) = ((1 * (n + 1)) / ((n ! ) * (n + 1))) by NEWTON: 15

        .= (1 / (n ! )) by XCMPLX_1: 91;



         A13: f is_differentiable_in x by A8, A6, Th46;

        hence ((1 / ((n + 1) ! )) (#) f) is_differentiable_in x by FDIFF_1: 15;



        thus ( diff (((1 / ((n + 1) ! )) (#) f),x)) = ((1 / ((n + 1) ! )) * ( diff (f,x))) by A13, FDIFF_1: 15

        .= ((( diff (f,x)) / ((n + 1) ! )) * 1) by XCMPLX_1: 75

        .= ((1 * ((n + 1) * ((x - a) |^ n))) / ((n + 1) ! )) by A8, A6, Th46

        .= (1 * (((x - a) |^ n) * ((n + 1) / ((n + 1) ! )))) by XCMPLX_1: 74

        .= (((x - a) |^ n) / (n ! )) by A12, XCMPLX_1: 99;

      end;

      ((1 / ((n + 1) ! )) (#) f) = g by A10, PARTFUN1: 5, A1, A5, A9;

      hence thesis by A11;

    end;



     Lm9: 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;



       A4: 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 f) = REAL by FUNCT_2:def 1;



       A6: ( dom (((r |^ (n + 1)) * L) (#) f)) = ( dom f) by VALUED_1:def 5;

       A7:

      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 A4

        .= (((r |^ (n + 1)) * (((x - a) |^ (n + 1)) / ((n + 1) ! ))) * L)

        .= ((((r |^ (n + 1)) * ((x - a) |^ (n + 1))) / ((n + 1) ! )) * L) by XCMPLX_1: 74

        .= ((((r * (x - a)) |^ (n + 1)) / ((n + 1) ! )) * L) by NEWTON: 7

        .= (g . x) by A1;

      end;



       A8: 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;



         A9: f is_differentiable_in x & ( diff (f,x)) = (((x - a) |^ n) / (n ! )) by Th47, A4;

        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 A9, FDIFF_1: 15

        .= (((r |^ (n + 1)) * (((x - a) |^ n) / (n ! ))) * L) by A9

        .= ((((r |^ (n + 1)) * ((x - a) |^ n)) / (n ! )) * L) by XCMPLX_1: 74

        .= ((((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) by XCMPLX_1: 74

        .= (r * ((((r * (x - a)) |^ n) / (n ! )) * L));

      end;

      (((r |^ (n + 1)) * L) (#) f) = g by A7, PARTFUN1: 5, A2, A5, A6;

      hence thesis by A8;

    end;



     Lm10: for m be non zero Element of NAT holds for 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;

      1 <= m by NAT_1: 14;

      then

      reconsider n = (m - 1) as Nat by INT_1: 5, ORDINAL1:def 12;

      reconsider n 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;



       A4: 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 f) = REAL by FUNCT_2:def 1;



       A6: ( dom (((r |^ (n + 2)) * L) (#) f)) = ( dom f) by VALUED_1:def 5;

       A7:

      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 A4

        .= (((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 |^ (n + 1)) * ((x - a) |^ (n + 1))) / ((n + 1) ! ))) * L) by XCMPLX_1: 74

        .= ((r * (((r * (x - a)) |^ (n + 1)) / ((n + 1) ! ))) * L) by NEWTON: 7

        .= (r * ((((r * (x - a)) |^ m) / (m ! )) * L))

        .= (g . x) by A1;

      end;



       A8: 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 Th47, A4;

        hence (((r |^ (n + 2)) * L) (#) f) is_differentiable_in x by FDIFF_1: 15;

      end;

      (((r |^ (n + 2)) * L) (#) f) = g by A7, A2, A5, A6, PARTFUN1: 5;

      hence thesis by A8;

    end;



     Lm11: for 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 a,r,t,L be Real, f0 be Function of REAL , REAL ;



       A1: a in REAL by XREAL_0:def 1;

      assume

       A2: a <= t;

      assume

       A3: for x be Real holds (f0 . x) = (r * ((((r * (x - a)) |^ n) / (n ! )) * L));



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



       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 A3, Lm10, 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;



       A7: 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;



       A8: ( dom g) = ( [#] REAL ) by FUNCT_2:def 1;

      for x be Real st x in ( [#] REAL ) holds g is_differentiable_in x by A7, Lm9;

      then

       A9: g is_differentiable_on REAL by A8;

       A10:

      now

        let x be Element of REAL ;

        assume x in ( dom (g `| ( [#] REAL )));



        thus ((g `| ( [#] REAL )) . x) = ( diff (g,x)) by A9, FDIFF_1:def 7

        .= (r * ((((r * (x - a)) |^ n) / (n ! )) * L)) by Lm9, A7

        .= (f0 . x) by A3

        .= ((f0 | ( [#] REAL )) . x);

      end;

      ( dom (g `| ( [#] REAL ))) = ( [#] REAL ) by A9, FDIFF_1:def 7

      .= ( dom (f0 | ( [#] REAL ))) by A4;

      then (g `| ( [#] REAL )) = (f0 | ( [#] REAL )) by A10, PARTFUN1: 5;

      then g in ( IntegralFuncs (f0,( [#] REAL ))) by A9, INTEGRA7:def 1;

      then

       A11: g is_integral_of (f0,( [#] REAL )) by INTEGRA7:def 2;



       A12: (f0 | ['a, t']) is bounded by INTEGRA5: 10, A5;



       A13: (g . t) = (( integral (f0,a,t)) + (g . a)) by A2, INTEGRA7: 18, A5, INTEGRA5: 11, A12, A11;



       A14: ( 0 qua Real + 1) <= (n + 1) by XREAL_1: 6;

      (g . a) = ( In (((((r * (a - a)) |^ (n + 1)) / ((n + 1) ! )) * L), REAL )) by A6, A1

      .= (( 0 qua Real / ((n + 1) ! )) * L) by A14, NEWTON: 11

      .= 0 qua Real;

      hence thesis by A12, A13, A5, INTEGRA5: 11, A7;

    end;



     Lm12: 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;

      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;



       A3: 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;



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



       A5: (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 Lm11, A1, A3;

      set f = (f0 | ['a, t']);



       A6: ( dom (f0 | ['a, t'])) = ['a, t'] by A4, RELAT_1: 62;

      reconsider f as continuous PartFunc of REAL , REAL by Lm11, A1, A3;

       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'])) by INTEGRA5:def 4, A1

      .= ( integral (f0 || ['a, t']));



       A11: ( integral (f,a,t)) = ( integral (f, ['a, t'])) by INTEGRA5:def 4, A1

      .= ( integral (f || ['a, t']));

      take f;

      thus thesis by A7, A11, A10, A5, A6;

    end;

    theorem :: ORDEQ_01:48



     Th48: for f,g be PartFunc of REAL , REAL st a <= t & ['a, t'] c= ( dom f) & f is_integrable_on ['a, t'] & (f | ['a, t']) is bounded & ['a, t'] c= ( dom g) & g is_integrable_on ['a, t'] & (g | ['a, t']) is bounded & for x be Real st x in ['a, t'] holds (f . x) <= (g . x) holds ( integral (f,a,t)) <= ( integral (g,a,t))

    proof

      let f,g be PartFunc of REAL , REAL ;

      assume

       A1: a <= t & ['a, t'] c= ( dom f) & f is_integrable_on ['a, t'] & (f | ['a, t']) is bounded & ['a, t'] c= ( dom g) & g is_integrable_on ['a, t'] & (g | ['a, t']) is bounded & for x be Real st x in ['a, t'] holds (f . x) <= (g . x);

      set f0 = (f | ['a, t']);

      set g0 = (g | ['a, t']);



       A2: ( dom f0) = ['a, t'] by A1, RELAT_1: 62;

      ( rng f0) c= REAL ;

      then

      reconsider f0 as Function of ['a, t'], REAL by A2, FUNCT_2: 2;



       A3: ( dom g0) = ['a, t'] by A1, RELAT_1: 62;

      ( rng g0) c= REAL ;

      then

      reconsider g0 as Function of ['a, t'], REAL by A3, FUNCT_2: 2;



       A4: (f0 | ['a, t']) is bounded by A1;



       A5: f0 is integrable by A1;



       A6: (g0 | ['a, t']) is bounded by A1;



       A7: g0 is integrable by A1;

      now

        let x be Real;

        assume

         A8: x in ['a, t'];



         A9: (f0 . x) = (f . x) by A8, FUNCT_1: 49;

        (g0 . x) = (g . x) by A8, FUNCT_1: 49;

        hence (f0 . x) <= (g0 . x) by A9, A1, A8;

      end;

      then

       A10: ( integral (f, ['a, t'])) <= ( integral (g, ['a, t'])) by A4, A5, A6, A7, INTEGRA2: 34;

      ( integral (f, ['a, t'])) = ( integral (f,a,t)) by A1, INTEGRA5:def 4;

      hence ( integral (f,a,t)) <= ( integral (g,a,t)) by A10, A1, INTEGRA5:def 4;

    end;

    definition

      let n be non zero Element of NAT ;

      let y0 be VECTOR of ( REAL-NS n), G be Function of ( REAL-NS n), ( REAL-NS n), a,b be Real;

      assume

       A1: a <= b & G is_continuous_on ( dom G);

      :: ORDEQ_01:def7

      func Fredholm (G,a,b,y0) -> Function of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))), ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) means

      : Def7: for x be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) holds ex f,g,Gf be continuous PartFunc of REAL , ( REAL-NS n) 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 , ( REAL-NS n) 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'],( REAL-NS n)));



         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 , ( REAL-NS n) such that

           A3: x = f0 & ( dom f0) = ['a, b'] by Def2;

          now

            let x0 be Real;

            assume

             A4: x0 in ( dom (G * f0));

            then x0 in ( dom f0) by FUNCT_1: 11;

            then

             A5: f0 is_continuous_in x0 by NFCONT_3:def 2;

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

            then (G | ( dom G)) is_continuous_in (f0 /. x0) by A1, NFCONT_1:def 7;

            hence (G * f0) is_continuous_in x0 by A4, A5, NFCONT_3: 15;

          end;

          then

          reconsider Gf = (G * f0) as continuous PartFunc of REAL , ( REAL-NS n) by NFCONT_3:def 2;

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

          then ( rng f0) c= ( dom G);

          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 , ( REAL-NS n) such that

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

          set F = (F0 | ['a, b']);



           A9: ( dom F) = (( dom F0) /\ ['a, b']) by RELAT_1: 61

          .= ( REAL /\ ['a, b']) by FUNCT_2:def 1

          .= ['a, b'] by XBOOLE_1: 28;

           A10:

          now

            let t be Real;

            assume

             A11: t in [.a, b.];



             A12: t in REAL by XREAL_0:def 1;



            thus (F . t) = (F0 . t) by A11, A9, A7, FUNCT_1: 47

            .= ( integral (Gf,a,t)) by A8, A12;

          end;



           A13: for t be Real st t in [.a, b.] holds F is_continuous_in t by Th34, A6, A1, A9, A10;

          set G0 = ( REAL --> y0);

          set G1 = (G0 | ['a, b']);



           A14: ( dom G1) = (( dom G0) /\ ['a, b']) by RELAT_1: 61

          .= ( REAL /\ ['a, b'])

          .= ['a, b'] by XBOOLE_1: 28;

           A15:

          now

            let t be Real;

            assume

             A16: t in [.a, b.];



            thus (G1 . t) = (G0 . t) by A16, A14, A7, FUNCT_1: 47

            .= y0 by XREAL_0:def 1, FUNCOP_1: 7;

          end;



           A17: F is continuous by A7, A9, A13, NFCONT_3:def 2;

          set g = (G1 + F);



           A18: ( dom g) = (( dom F) /\ ( dom G1)) by VFUNCT_1:def 1

          .= ['a, b'] by A9, A14;

          reconsider g as continuous PartFunc of REAL , ( REAL-NS n) by A17;

          reconsider y = g as Element of D by A18, Def2;

          take y;

          now

            let t be Real;

            assume

             A19: t in ['a, b'];



             A20: (G1 /. t) = (G1 . t) by A19, A14, PARTFUN1:def 6

            .= y0 by A19, A7, A15;



             A21: (F /. t) = (F . t) by A19, A9, PARTFUN1:def 6

            .= ( integral (Gf,a,t)) by A19, A7, A10;



            thus (g . t) = (g /. t) by A18, A19, PARTFUN1:def 6

            .= (y0 + ( integral (Gf,a,t))) by A20, A21, A18, A19, VFUNCT_1:def 1;

          end;

          hence thesis by A18, A3;

        end;

        consider F be Function of D, D such that

         A22: for x be Element of D holds P[x, (F . x)] from FUNCT_2:sch 3( A2);

        take F;

        thus thesis by A22;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))), ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n)));

        assume

         A23: for x be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) holds ex f,g,Gf be continuous PartFunc of REAL , ( REAL-NS n) 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

         A24: for x be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) holds ex f,g,Gf be continuous PartFunc of REAL , ( REAL-NS n) 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'],( REAL-NS n)));

          consider f1,g1,Gf1 be continuous PartFunc of REAL , ( REAL-NS n) such that

           A25: 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 A23;

          consider f2,g2,Gf2 be continuous PartFunc of REAL , ( REAL-NS n) such that

           A26: 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 A24;

          now

            let t be object;

            assume

             A27: t in ( dom g1);

            then

            reconsider t0 = t as Real;



            thus (g1 . t) = (y0 + ( integral (Gf2,a,t0))) by A26, A27, A25

            .= (g2 . t) by A27, A26, A25;

          end;

          hence (F1 . x) = (F2 . x) by A25, A26, FUNCT_1: 2;

        end;

        hence F1 = F2 by FUNCT_2:def 8;

      end;

    end

    theorem :: ORDEQ_01:49



     Th49: a <= b & 0 < r & (for y1,y2 be VECTOR of ( REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||)) implies for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))), g,h be continuous PartFunc of REAL , ( REAL-NS n) 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 ( REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||);



       A2: ( dom G) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

      for x1,x2 be Point of ( REAL-NS n) st x1 in the carrier of ( REAL-NS n) & x2 in the carrier of ( REAL-NS n) holds ||.((G /. x1) - (G /. x2)).|| <= (r * ||.(x1 - x2).||) by A1;

      then G is_Lipschitzian_on the carrier of ( REAL-NS n) by A1, A2, NFCONT_1:def 9;

      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'],( REAL-NS n))), g,h be continuous PartFunc of REAL , ( REAL-NS n);

      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 , ( REAL-NS n) 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 Def7, A1, A3;

      consider f2,g2,Gf2 be continuous PartFunc of REAL , ( REAL-NS n) 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 Def7, A1, A3;

      set Gf12 = (Gf1 - Gf2);



       A7: ( dom G) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

      then ( rng f1) c= ( dom G);

      then

       A8: ( dom Gf1) = ['a, b'] by A5, RELAT_1: 27;

      ( rng f2) c= ( dom G) by A7;

      then

       A9: ( dom Gf2) = ['a, b'] by A6, RELAT_1: 27;

      reconsider Gf12 as continuous PartFunc of REAL , ( REAL-NS n);



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

      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;



       A13: ( dom Gf12) = (( dom Gf1) /\ ( dom Gf2)) by VFUNCT_1:def 2

      .= ['a, b'] by A8, A9;



       A14: Gf12 is_integrable_on ['a, b'] by A13, Th33;



       A15: (Gf12 | ['a, b']) is bounded by A13, Th32;

      (Gf12 | ['a, b']) is continuous;

      then

       A16: ( ||.Gf12.|| | ['a, b']) is continuous by A13, NFCONT_3: 22;

       ['a, b'] = ( dom ||.Gf12.||) by A13, NORMSP_0:def 2;

      then

       A17: ||.Gf12.|| is_integrable_on ['a, b'] by A16, INTEGRA5: 11;



       A18: a in ['a, b'] by A10, A1;

      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'];



         A20: ['a, t'] c= ['a, b'] by A12, INTEGR19: 1;



         A21: (Gf12 /. x) = ((Gf1 /. x) - (Gf2 /. x)) by A13, A20, A19, VFUNCT_1:def 2;



         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;



         A23: (Gf2 /. x) = (Gf2 . x) by A9, A20, A19, PARTFUN1:def 6

        .= (G . (f2 . x)) by A20, A19, A9, A6, FUNCT_1: 12

        .= (G /. (f2 /. x)) by A20, A19, A6, PARTFUN1:def 6;



         A24: ||.((Gf1 /. x) - (Gf2 /. x)).|| <= (r * ||.((f1 /. x) - (f2 /. x)).||) by A22, A23, A1;

         ||.((f1 /. x) - (f2 /. x)).|| <= ||.(u - v).|| by A20, A19, A5, A6, Th26;

        then (r * ||.((f1 /. x) - (f2 /. x)).||) <= (r * ||.(u - v).||) by A1, XREAL_1: 64;

        hence thesis by A21, A24, XXREAL_0: 2;

      end;

      then

       A25: ||.( integral (Gf12,a,t)).|| <= ((r * ||.(u - v).||) * (t - a)) by Th45, A1, A17, A14, A15, A13, A18, A11, A12;



       A26: Gf1 is_integrable_on ['a, b'] by A8, Th33;



       A27: (Gf1 | ['a, b']) is bounded by A8, Th32;



       A28: Gf2 is_integrable_on ['a, b'] by A9, Th33;



       A29: (Gf2 | ['a, b']) is bounded by A9, Th32;



       A30: ( integral (Gf12,a,t)) = (( integral (Gf1,a,t)) - ( integral (Gf2,a,t))) by A8, A9, A26, A27, A28, A29, A18, A11, A1, INTEGR19: 50;



       A31: (g /. t) = (g1 . t) by A4, A11, A5, PARTFUN1:def 6

      .= (y0 + ( integral (Gf1,a,t))) by A5, A11;



       A32: (h /. t) = (g2 . t) by A4, A11, A6, PARTFUN1:def 6

      .= (y0 + ( integral (Gf2,a,t))) by A6, A11;

      ((g /. t) - (h /. t)) = (((y0 + ( integral (Gf1,a,t))) - y0) - ( integral (Gf2,a,t))) by A31, A32, RLVECT_1: 27

      .= ((( integral (Gf1,a,t)) + (y0 - y0)) - ( integral (Gf2,a,t))) by RLVECT_1: 28

      .= ((( integral (Gf1,a,t)) + ( 0. ( REAL-NS n))) - ( integral (Gf2,a,t))) by RLVECT_1: 15

      .= ( integral (Gf12,a,t)) by A30;

      hence thesis by A25;

    end;

    theorem :: ORDEQ_01:50



     Th50: a <= b & 0 < r & (for y1,y2 be VECTOR of ( REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||)) implies for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))), m be Element of NAT , g,h be continuous PartFunc of REAL , ( REAL-NS n) 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 ( REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||);

      set F = ( Fredholm (G,a,b,y0));



       A2: ( dom G) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

      for x1,x2 be Point of ( REAL-NS n) st x1 in the carrier of ( REAL-NS n) & x2 in the carrier of ( REAL-NS n) holds ||.((G /. x1) - (G /. x2)).|| <= (r * ||.(x1 - x2).||) by A1;

      then G is_Lipschitzian_on the carrier of ( REAL-NS n) by A1, A2, NFCONT_1:def 9;

      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'],( REAL-NS n)));

      defpred P[ Nat] means for g,h be continuous PartFunc of REAL , ( REAL-NS n) 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 , ( REAL-NS n);

        assume

         A5: g = (( iter (F,( 0 qua Element of NAT + 1))) . u1) & h = (( iter (F,( 0 qua Element of NAT + 1))) . v1);



         A6: g = (F . u1) by A5, FUNCT_7: 70;



         A7: h = (F . v1) by A5, 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, Th49, A1, A6, A7;

        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 , ( REAL-NS n);

        assume

         A10: g = (( iter (F,((k + 1) + 1))) . u1) & h = (( iter (F,((k + 1) + 1))) . v1);

        reconsider u = (( iter (F,(k + 1))) . u1) as VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n)));

        reconsider v = (( iter (F,(k + 1))) . v1) as VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n)));



         A11: ( dom ( iter (F,(k + 1)))) = the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) 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 , ( REAL-NS n) 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 Def7, A1, A3;

        consider f2,g2,Gf2 be continuous PartFunc of REAL , ( REAL-NS n) 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 Def7, A1, A3;

        set Gf12 = (Gf1 - Gf2);



         A16: for t be Real st t in ['a, b'] holds ||.((f1 /. t) - (f2 /. t)).|| <= ((((r * (t - a)) |^ (k + 1)) / ((k + 1) ! )) * ||.(u1 - v1).||) by A9, A14, A15;



         A17: ( dom G) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

        then ( rng f1) c= ( dom G);

        then

         A18: ( dom Gf1) = ['a, b'] by A14, RELAT_1: 27;

        ( rng f2) c= ( dom G) by A17;

        then

         A19: ( dom Gf2) = ['a, b'] by A15, RELAT_1: 27;

        reconsider Gf12 as continuous PartFunc of REAL , ( REAL-NS n);



         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;



         A23: ex g be Element of REAL st t = g & a <= g & g <= b

        proof

          consider g be Real such that

           A24: 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 A24;

        end;



         A25: ( dom Gf12) = (( dom Gf1) /\ ( dom Gf2)) by VFUNCT_1:def 2

        .= ['a, b'] by A18, A19;

        then

         A26: ( dom ||.Gf12.||) = ['a, b'] by NORMSP_0:def 2;



         A27: Gf12 is_integrable_on ['a, b'] by A25, Th33;



         A28: (Gf12 | ['a, b']) is bounded by A25, Th32;



         A29: a in ['a, b'] by A20, A1;

        (Gf12 | ['a, b']) is continuous;

        then

         A30: ( ||.Gf12.|| | ['a, b']) is continuous by A25, NFCONT_3: 22;

         ['a, b'] = ( dom ||.Gf12.||) by A25, NORMSP_0:def 2;

        then

         A31: ||.Gf12.|| is_integrable_on ['a, b'] by A30, INTEGRA5: 11;

        ( min (a,t)) = a & ( max (a,t)) = t by A22, XXREAL_0:def 9, XXREAL_0:def 10;

        then

         A32: ||.Gf12.|| is_integrable_on ['a, t'] & ( ||.Gf12.|| | ['a, t']) is bounded & ||.( integral (Gf12,a,t)).|| <= ( integral ( ||.Gf12.||,a,t)) by A1, A27, A28, A25, A29, A21, A31, Th44;



         A33: (k + 1) is non zero Element of NAT by ORDINAL1:def 12;

        consider rg be PartFunc of REAL , REAL such that

         A34: ( 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 Lm12, A23, A33;



         A35: ['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

           A36: x in ['a, t'];



           A37: (Gf12 /. x) = ((Gf1 /. x) - (Gf2 /. x)) by A25, A35, A36, VFUNCT_1:def 2;



           A38: (Gf1 /. x) = (Gf1 . x) by A18, A35, A36, PARTFUN1:def 6

          .= (G . (f1 . x)) by A35, A36, A18, A14, FUNCT_1: 12

          .= (G /. (f1 /. x)) by A35, A36, A14, PARTFUN1:def 6;



           A39: (Gf2 /. x) = (Gf2 . x) by A19, A35, A36, PARTFUN1:def 6

          .= (G . (f2 . x)) by A35, A36, A19, A15, FUNCT_1: 12

          .= (G /. (f2 /. x)) by A35, A36, A15, PARTFUN1:def 6;



           A40: ||.((Gf1 /. x) - (Gf2 /. x)).|| <= (r * ||.((f1 /. x) - (f2 /. x)).||) by A38, A39, A1;

          (r * ||.((f1 /. x) - (f2 /. x)).||) <= (r * ((((r * (x - a)) |^ (k + 1)) / ((k + 1) ! )) * ||.(u1 - v1).||)) by A1, XREAL_1: 64, A16, A35, A36;

          then (r * ||.((f1 /. x) - (f2 /. x)).||) <= (rg . x) by A36, A34;

          then ||.((Gf1 /. x) - (Gf2 /. x)).|| <= (rg . x) by A40, XXREAL_0: 2;

          hence thesis by A26, A35, A36, NORMSP_0:def 2, A37;

        end;

        then

         A41: ( integral ( ||.Gf12.||,a,t)) <= ( integral (rg,a,t)) by A32, A22, A26, A35, A34, Th48;



         A42: Gf1 is_integrable_on ['a, b'] by A18, Th33;



         A43: (Gf1 | ['a, b']) is bounded by A18, Th32;



         A44: Gf2 is_integrable_on ['a, b'] by A19, Th33;



         A45: (Gf2 | ['a, b']) is bounded by A19, Th32;



         A46: ( integral (Gf12,a,t)) = (( integral (Gf1,a,t)) - ( integral (Gf2,a,t))) by A18, A19, A42, A43, A44, A45, A29, A21, A1, INTEGR19: 50;



         A47: (g /. t) = (g1 . t) by A12, A10, A21, A14, PARTFUN1:def 6

        .= (y0 + ( integral (Gf1,a,t))) by A14, A21;



         A48: (h /. t) = (g2 . t) by A13, A10, A21, A15, PARTFUN1:def 6

        .= (y0 + ( integral (Gf2,a,t))) by A15, A21;

        ((g /. t) - (h /. t)) = (((y0 + ( integral (Gf1,a,t))) - y0) - ( integral (Gf2,a,t))) by RLVECT_1: 27, A47, A48

        .= ((( integral (Gf1,a,t)) + (y0 - y0)) - ( integral (Gf2,a,t))) by RLVECT_1: 28

        .= ((( integral (Gf1,a,t)) + ( 0. ( REAL-NS n))) - ( integral (Gf2,a,t))) by RLVECT_1: 15

        .= ( integral (Gf12,a,t)) by A46;

        hence thesis by A41, A32, XXREAL_0: 2, A34;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A8);

      hence thesis;

    end;



     Lm13: 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;



     Lm14: 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

       A2: s is convergent & ( lim s) = 0 by SERIES_1: 4;

      consider n be Nat such that

       A3: for m be Nat st n <= m holds |.((s . m) - 0 ).| < 1 by A2, 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_01:51



     Th51: for m be Nat st a <= b & 0 < r & (for y1,y2 be VECTOR of ( REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||)) holds for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) 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 ( REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= (r * ||.(y1 - y2).||);

      let u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n)));

      reconsider u1 = (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . u) as VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n)));

      reconsider v1 = (( iter (( Fredholm (G,a,b,y0)),(m + 1))) . v) as VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n)));

      consider g be continuous PartFunc of REAL , ( REAL-NS n) such that

       A2: u1 = g & ( dom g) = ['a, b'] by Def2;

      consider h be continuous PartFunc of REAL , ( REAL-NS n) such that

       A3: v1 = h & ( dom h) = ['a, b'] by Def2;

      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, Th50, A1, A2, A3;

        ((((r * (t - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) <= ((((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) by A6, A1, Lm13;

        hence ||.((g /. t) - (h /. t)).|| <= ((((r * (b - a)) |^ (m + 1)) / ((m + 1) ! )) * ||.(u - v).||) by A7, XXREAL_0: 2;

      end;

      hence thesis by Th27, A2, A3;

    end;

    theorem :: ORDEQ_01:52



     Th52: a < b & G is_Lipschitzian_on the carrier of ( REAL-NS n) 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 ( REAL-NS n);

      then

      consider r be Real such that

       A2: 0 < r & for x1,x2 be Point of ( REAL-NS n) st x1 in the carrier of ( REAL-NS n) & x2 in the carrier of ( REAL-NS n) holds ||.((G /. x1) - (G /. x2)).|| <= (r * ||.(x1 - x2).||) by NFCONT_1:def 9;



       A3: for x1,x2 be Point of ( REAL-NS n) 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 Lm14, A1, A2;

      take m;

      for u,v be VECTOR of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) 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 Th51, A3, A2, A1;

      hence thesis by A4;

    end;

    theorem :: ORDEQ_01:53



     Th53: a < b & G is_Lipschitzian_on the carrier of ( REAL-NS n) implies ( Fredholm (G,a,b,y0)) is with_unique_fixpoint

    proof

      assume a < b & G is_Lipschitzian_on the carrier of ( REAL-NS n);

      then ex m be Nat st ( iter (( Fredholm (G,a,b,y0)),(m + 1))) is contraction by Th52;

      hence thesis by Th7;

    end;

    theorem :: ORDEQ_01:54



     Th54: for f,g be continuous PartFunc of REAL , ( REAL-NS n) st ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Z = ].a, b.[ & a < b & G is_Lipschitzian_on the carrier of ( REAL-NS n) & 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 , ( REAL-NS n);

      assume

       A1: ( dom f) = ['a, b'] & ( dom g) = ['a, b'] & Z = ].a, b.[ & a < b & G is_Lipschitzian_on the carrier of ( REAL-NS n) & g = (( Fredholm (G,a,b,y0)) . f);

      set D = ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n)));

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

      then

       A2: G is_continuous_on ( dom G) by A1, NFCONT_1: 45;

      f is Element of D by Def2, A1;

      then

      consider f0,g0,Gf0 be continuous PartFunc of REAL , ( REAL-NS n) 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, Def7;

      reconsider Gf = (G * f) as continuous PartFunc of REAL , ( REAL-NS n) by A3;

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

      then ( rng f) c= ( dom G);

      then ( dom Gf) = ['a, b'] by A1, RELAT_1: 27;

      hence thesis by A1, Th36, A3;

    end;

    theorem :: ORDEQ_01:55



     Th55: for y be continuous PartFunc of REAL , ( REAL-NS n) st a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of ( REAL-NS n) & ( 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 , ( REAL-NS n);

      assume

       A1: a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of ( REAL-NS n) & ( 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)));



       A2: ( dom ( Fredholm (G,a,b,y0))) = the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) by FUNCT_2:def 1;



       A3: y is Element of the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) by Def2, A1;



       A4: y in ( dom ( Fredholm (G,a,b,y0))) by A2, Def2, A1;

      ( dom G) = the carrier of ( REAL-NS n) 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 , ( REAL-NS n) 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 Def7, A1, A3;

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

      then ( rng f) c= ( dom G);

      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;



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



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



        thus ( diff (y,t)) = (G . (y /. t)) by A1, A7

        .= (G . (y . t)) by A8, A1, A7, A9, PARTFUN1:def 6

        .= (Gf . t) by A5, A8, A1, A7, A9, FUNCT_1: 13

        .= (Gf /. t) by A5, A8, A1, A7, A9, A6, PARTFUN1:def 6;

      end;

      hence thesis by A4, A5, Th43, A1, A6;

    end;

    theorem :: ORDEQ_01:56

    for y1,y2 be continuous PartFunc of REAL , ( REAL-NS n) st a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of ( REAL-NS n) & ( 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 , ( REAL-NS n);

      assume

       A1: a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of ( REAL-NS n) & ( 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 Th53;

      then

      consider y be set such that

       A2: 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;



       A3: y1 is_a_fixpoint_of ( Fredholm (G,a,b,y0)) by Th55, A1;



       A4: y2 is_a_fixpoint_of ( Fredholm (G,a,b,y0)) by Th55, A1;

      y1 = y by A3, A2

      .= y2 by A4, A2;

      hence thesis;

    end;

    theorem :: ORDEQ_01:57

    a < b & Z = ].a, b.[ & G is_Lipschitzian_on the carrier of ( REAL-NS n) implies ex y be continuous PartFunc of REAL , ( REAL-NS n) 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 ( REAL-NS n);

      then ( Fredholm (G,a,b,y0)) is with_unique_fixpoint by Th53;

      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;



       A3: x in ( dom ( Fredholm (G,a,b,y0))) & x = (( Fredholm (G,a,b,y0)) . x) by A2;

      reconsider x as Element of the carrier of ( R_NormSpace_of_ContinuousFunctions ( ['a, b'],( REAL-NS n))) by A3;

      consider f be continuous PartFunc of REAL , ( REAL-NS n) such that

       A4: x = f & ( dom f) = ['a, b'] by Def2;

      take f;

      thus ( dom f) = ['a, b'] & f is_differentiable_on Z & (f /. a) = y0 by Th54, A4, A1, A3;



       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 ( REAL-NS n) 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, Th54, A4, A1, A3

      .= ((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;