nfcont_2.miz



    begin

    reserve n,m for Nat,

x,X,X1 for set,

s,g,r,p for Real,

S,T for RealNormSpace,

f,f1,f2 for PartFunc of S, T,

s1,s2,q1 for sequence of S,

x0,x1,x2 for Point of S,

Y for Subset of S;

    definition

      let X, S, T;

      let f;

      :: NFCONT_2:def1

      pred f is_uniformly_continuous_on X means X c= ( dom f) & for r st 0 < r holds ex s st 0 < s & for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r;

    end

    definition

      let X, S;

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

      :: NFCONT_2:def2

      pred f is_uniformly_continuous_on X means X c= ( dom f) & for r st 0 < r holds ex s st 0 < s & for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds |.((f /. x1) - (f /. x2)).| < r;

    end

    theorem :: NFCONT_2:1

    

     Th1: f is_uniformly_continuous_on X & X1 c= X implies f is_uniformly_continuous_on X1

    proof

      assume that

       A1: f is_uniformly_continuous_on X and

       A2: X1 c= X;

      X c= ( dom f) by A1;

      hence X1 c= ( dom f) by A2, XBOOLE_1: 1;

      let r;

      assume 0 < r;

      then

      consider s such that

       A3: 0 < s and

       A4: for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1;

      take s;

      thus 0 < s by A3;

      let x1, x2;

      assume x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s;

      hence thesis by A2, A4;

    end;

    theorem :: NFCONT_2:2

    f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies (f1 + f2) is_uniformly_continuous_on (X /\ X1)

    proof

      assume that

       A1: f1 is_uniformly_continuous_on X and

       A2: f2 is_uniformly_continuous_on X1;

      

       A3: f2 is_uniformly_continuous_on (X /\ X1) by A2, Th1, XBOOLE_1: 17;

      then

       A4: (X /\ X1) c= ( dom f2);

      

       A5: f1 is_uniformly_continuous_on (X /\ X1) by A1, Th1, XBOOLE_1: 17;

      then (X /\ X1) c= ( dom f1);

      then (X /\ X1) c= (( dom f1) /\ ( dom f2)) by A4, XBOOLE_1: 19;

      hence

       A6: (X /\ X1) c= ( dom (f1 + f2)) by VFUNCT_1:def 1;

      let r;

      assume 0 < r;

      then

       A7: 0 < (r / 2) by XREAL_1: 215;

      then

      consider s such that

       A8: 0 < s and

       A9: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) & ||.(x1 - x2).|| < s holds ||.((f1 /. x1) - (f1 /. x2)).|| < (r / 2) by A5;

      consider g such that

       A10: 0 < g and

       A11: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) & ||.(x1 - x2).|| < g holds ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) by A3, A7;

      take p = ( min (s,g));

      thus 0 < p by A8, A10, XXREAL_0: 15;

      let x1, x2;

      assume that

       A12: x1 in (X /\ X1) and

       A13: x2 in (X /\ X1) and

       A14: ||.(x1 - x2).|| < p;

      p <= g by XXREAL_0: 17;

      then ||.(x1 - x2).|| < g by A14, XXREAL_0: 2;

      then

       A15: ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) by A11, A12, A13;

      p <= s by XXREAL_0: 17;

      then ||.(x1 - x2).|| < s by A14, XXREAL_0: 2;

      then ||.((f1 /. x1) - (f1 /. x2)).|| < (r / 2) by A9, A12, A13;

      then

       A16: ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) < ((r / 2) + (r / 2)) by A15, XREAL_1: 8;

      

       A17: ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| <= ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) by NORMSP_1:def 1;

       ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A6, A12, VFUNCT_1:def 1

      .= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A6, A13, VFUNCT_1:def 1

      .= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:def 3

      .= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1: 27

      .= ||.((f1 /. x1) + ((( - (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).||

      .= ||.((f1 /. x1) + (( - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def 3

      .= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def 3;

      hence thesis by A16, A17, XXREAL_0: 2;

    end;

    theorem :: NFCONT_2:3

    f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies (f1 - f2) is_uniformly_continuous_on (X /\ X1)

    proof

      assume that

       A1: f1 is_uniformly_continuous_on X and

       A2: f2 is_uniformly_continuous_on X1;

      

       A3: f2 is_uniformly_continuous_on (X /\ X1) by A2, Th1, XBOOLE_1: 17;

      then

       A4: (X /\ X1) c= ( dom f2);

      

       A5: f1 is_uniformly_continuous_on (X /\ X1) by A1, Th1, XBOOLE_1: 17;

      then (X /\ X1) c= ( dom f1);

      then (X /\ X1) c= (( dom f1) /\ ( dom f2)) by A4, XBOOLE_1: 19;

      hence

       A6: (X /\ X1) c= ( dom (f1 - f2)) by VFUNCT_1:def 2;

      let r;

      assume 0 < r;

      then

       A7: 0 < (r / 2) by XREAL_1: 215;

      then

      consider s such that

       A8: 0 < s and

       A9: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) & ||.(x1 - x2).|| < s holds ||.((f1 /. x1) - (f1 /. x2)).|| < (r / 2) by A5;

      consider g such that

       A10: 0 < g and

       A11: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) & ||.(x1 - x2).|| < g holds ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) by A3, A7;

      take p = ( min (s,g));

      thus 0 < p by A8, A10, XXREAL_0: 15;

      let x1, x2;

      assume that

       A12: x1 in (X /\ X1) and

       A13: x2 in (X /\ X1) and

       A14: ||.(x1 - x2).|| < p;

      p <= g by XXREAL_0: 17;

      then ||.(x1 - x2).|| < g by A14, XXREAL_0: 2;

      then

       A15: ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) by A11, A12, A13;

      p <= s by XXREAL_0: 17;

      then ||.(x1 - x2).|| < s by A14, XXREAL_0: 2;

      then ||.((f1 /. x1) - (f1 /. x2)).|| < (r / 2) by A9, A12, A13;

      then

       A16: ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) < ((r / 2) + (r / 2)) by A15, XREAL_1: 8;

      

       A17: ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| <= ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) by NORMSP_1: 3;

       ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A6, A12, VFUNCT_1:def 2

      .= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A6, A13, VFUNCT_1:def 2

      .= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1: 27

      .= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def 3

      .= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def 3

      .= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1: 27;

      hence thesis by A16, A17, XXREAL_0: 2;

    end;

    theorem :: NFCONT_2:4

    

     Th4: f is_uniformly_continuous_on X implies (p (#) f) is_uniformly_continuous_on X

    proof

      assume

       A1: f is_uniformly_continuous_on X;

      then X c= ( dom f);

      hence

       A2: X c= ( dom (p (#) f)) by VFUNCT_1:def 4;

      now

        per cases ;

          suppose

           A3: p = 0 ;

          let r;

          assume

           A4: 0 < r;

          then

          consider s such that

           A5: 0 < s and for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1;

          take s;

          thus 0 < s by A5;

          let x1, x2;

          assume that

           A6: x1 in X and

           A7: x2 in X and ||.(x1 - x2).|| < s;

           ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A2, A6, VFUNCT_1:def 4

          .= ||.(( 0. T) - ((p (#) f) /. x2)).|| by A3, RLVECT_1: 10

          .= ||.(( 0. T) - (p * (f /. x2))).|| by A2, A7, VFUNCT_1:def 4

          .= ||.(( 0. T) - ( 0. T)).|| by A3, RLVECT_1: 10

          .= ||.( 0. T).|| by RLVECT_1: 13

          .= 0 by NORMSP_0:def 6;

          hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r by A4;

        end;

          suppose

           A8: p <> 0 ;

          then

           A9: 0 <> |.p.| by COMPLEX1: 47;

          let r;

          

           A10: 0 < |.p.| by A8, COMPLEX1: 47;

          assume 0 < r;

          then 0 < (r / |.p.|) by A10, XREAL_1: 139;

          then

          consider s such that

           A11: 0 < s and

           A12: for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < (r / |.p.|) by A1;

          take s;

          thus 0 < s by A11;

          let x1, x2;

          assume that

           A13: x1 in X and

           A14: x2 in X and

           A15: ||.(x1 - x2).|| < s;

          

           A16: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A2, A13, VFUNCT_1:def 4

          .= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A2, A14, VFUNCT_1:def 4

          .= ||.(p * ((f /. x1) - (f /. x2))).|| by RLVECT_1: 34

          .= ( |.p.| * ||.((f /. x1) - (f /. x2)).||) by NORMSP_1:def 1;

          ( |.p.| * ||.((f /. x1) - (f /. x2)).||) < ((r / |.p.|) * |.p.|) by A10, A12, A13, A14, A15, XREAL_1: 68;

          hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r by A9, A16, XCMPLX_1: 87;

        end;

      end;

      hence thesis;

    end;

    theorem :: NFCONT_2:5

    f is_uniformly_continuous_on X implies ( - f) is_uniformly_continuous_on X

    proof

      

       A1: ( - f) = (( - 1) (#) f) by VFUNCT_1: 23;

      assume f is_uniformly_continuous_on X;

      hence thesis by A1, Th4;

    end;

    theorem :: NFCONT_2:6

    f is_uniformly_continuous_on X implies ||.f.|| is_uniformly_continuous_on X

    proof

      assume

       A1: f is_uniformly_continuous_on X;

      then X c= ( dom f);

      hence

       A2: X c= ( dom ||.f.||) by NORMSP_0:def 3;

      let r;

      assume 0 < r;

      then

      consider s such that

       A3: 0 < s and

       A4: for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1;

      take s;

      thus 0 < s by A3;

      let x1, x2;

      assume that

       A5: x1 in X and

       A6: x2 in X and

       A7: ||.(x1 - x2).|| < s;

       |.(( ||.f.|| /. x1) - ( ||.f.|| /. x2)).| = |.(( ||.f.|| . x1) - ( ||.f.|| /. x2)).| by A2, A5, PARTFUN1:def 6

      .= |.(( ||.f.|| . x1) - ( ||.f.|| . x2)).| by A2, A6, PARTFUN1:def 6

      .= |.( ||.(f /. x1).|| - ( ||.f.|| . x2)).| by A2, A5, NORMSP_0:def 3

      .= |.( ||.(f /. x1).|| - ||.(f /. x2).||).| by A2, A6, NORMSP_0:def 3;

      then

       A8: |.(( ||.f.|| /. x1) - ( ||.f.|| /. x2)).| <= ||.((f /. x1) - (f /. x2)).|| by NORMSP_1: 9;

       ||.((f /. x1) - (f /. x2)).|| < r by A4, A5, A6, A7;

      hence thesis by A8, XXREAL_0: 2;

    end;

    theorem :: NFCONT_2:7

    

     Th7: f is_uniformly_continuous_on X implies f is_continuous_on X

    proof

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0;

        let r be Real;

        assume that

         A3: x0 in X and

         A4: 0 < r;

        consider s be Real such that

         A5: 0 < s and

         A6: for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1, A4;

        take s;

        thus 0 < s by A5;

        let x1;

        assume x1 in X & ||.(x1 - x0).|| < s;

        hence ||.((f /. x1) - (f /. x0)).|| < r by A3, A6;

      end;

      X c= ( dom f) by A1;

      hence thesis by A2, NFCONT_1: 19;

    end;

    theorem :: NFCONT_2:8

    

     Th8: for f be PartFunc of the carrier of S, REAL st f is_uniformly_continuous_on X holds f is_continuous_on X

    proof

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

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0;

        let r be Real;

        assume that

         A3: x0 in X and

         A4: 0 < r;

        consider s be Real such that

         A5: 0 < s and

         A6: for x1, x2 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds |.((f /. x1) - (f /. x2)).| < r by A1, A4;

        take s;

        thus 0 < s by A5;

        let x1;

        assume x1 in X & ||.(x1 - x0).|| < s;

        hence |.((f /. x1) - (f /. x0)).| < r by A3, A6;

      end;

      X c= ( dom f) by A1;

      hence thesis by A2, NFCONT_1: 20;

    end;

    theorem :: NFCONT_2:9

    

     Th9: f is_Lipschitzian_on X implies f is_uniformly_continuous_on X

    proof

      assume

       A1: f is_Lipschitzian_on X;

      hence X c= ( dom f) by NFCONT_1:def 9;

      consider r be Real such that

       A2: 0 < r and

       A3: for x1, x2 st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= (r * ||.(x1 - x2).||) by A1, NFCONT_1:def 9;

      let p be Real such that

       A4: 0 < p;

      take s = (p / r);

      thus 0 < s by A2, A4, XREAL_1: 139;

      let x1, x2;

      assume x1 in X & x2 in X & ||.(x1 - x2).|| < s;

      then (r * ||.(x1 - x2).||) < (s * r) & ||.((f /. x1) - (f /. x2)).|| <= (r * ||.(x1 - x2).||) by A2, A3, XREAL_1: 68;

      then ||.((f /. x1) - (f /. x2)).|| < ((p / r) * r) by XXREAL_0: 2;

      hence thesis by A2, XCMPLX_1: 87;

    end;

    theorem :: NFCONT_2:10

    for f, Y st Y is compact & f is_continuous_on Y holds f is_uniformly_continuous_on Y

    proof

      let f, Y such that

       A1: Y is compact and

       A2: f is_continuous_on Y;

      

       A3: Y c= ( dom f) by A2, NFCONT_1:def 7;

      assume not thesis;

      then

      consider r such that

       A4: 0 < r and

       A5: for s st 0 < s holds ex x1, x2 st x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r by A3;

      defpred P[ Nat, Point of S] means $2 in Y & ex x2 st x2 in Y & ||.($2 - x2).|| < (1 / ($1 + 1)) & not ||.((f /. $2) - (f /. x2)).|| < r;

      

       A6: for n holds 0 < (1 / (n + 1)) by XREAL_1: 139;

       A7:

      now

        let n be Element of NAT ;

        consider x1 such that

         A8: ex x2 st x1 in Y & x2 in Y & ||.(x1 - x2).|| < (1 / (n + 1)) & not ||.((f /. x1) - (f /. x2)).|| < r by A5, A6;

        take x1;

        thus P[n, x1] by A8;

      end;

      consider s1 such that

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

      defpred P[ Nat, Point of S] means $2 in Y & ||.((s1 . $1) - $2).|| < (1 / ($1 + 1)) & not ||.((f /. (s1 . $1)) - (f /. $2)).|| < r;

      

       A10: for n be Element of NAT holds ex x2 st P[n, x2] by A9;

      consider s2 such that

       A11: for n be Element of NAT holds P[n, (s2 . n)] from FUNCT_2:sch 3( A10);

      now

        let x be object;

        assume x in ( rng s1);

        then

        consider n such that

         A12: x = (s1 . n) by NFCONT_1: 6;

        n in NAT by ORDINAL1:def 12;

        hence x in Y by A9, A12;

      end;

      then

       A13: ( rng s1) c= Y by TARSKI:def 3;

      then

      consider q1 such that

       A14: q1 is subsequence of s1 and

       A15: q1 is convergent and

       A16: ( lim q1) in Y by A1, NFCONT_1:def 2;

      consider Ns1 be increasing sequence of NAT such that

       A17: q1 = (s1 * Ns1) by A14, VALUED_0:def 17;

      set q2 = (q1 - ((s1 - s2) * Ns1));

      

       A18: (f | Y) is_continuous_in ( lim q1) by A2, A16, NFCONT_1:def 7;

      now

        let x be object;

        assume x in ( rng s2);

        then

        consider n such that

         A19: x = (s2 . n) by NFCONT_1: 6;

        n in NAT by ORDINAL1:def 12;

        hence x in Y by A11, A19;

      end;

      then

       A20: ( rng s2) c= Y by TARSKI:def 3;

      now

        let n be Element of NAT ;

        

        thus (q2 . n) = (((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n)) by A17, NORMSP_1:def 3

        .= ((s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n)) by FUNCT_2: 15

        .= ((s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n))) by FUNCT_2: 15

        .= ((s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n)))) by NORMSP_1:def 3

        .= (((s1 . (Ns1 . n)) - (s1 . (Ns1 . n))) + (s2 . (Ns1 . n))) by RLVECT_1: 29

        .= (( 0. S) + (s2 . (Ns1 . n))) by RLVECT_1: 15

        .= (s2 . (Ns1 . n)) by RLVECT_1: 4

        .= ((s2 * Ns1) . n) by FUNCT_2: 15;

      end;

      then

       A21: q2 = (s2 * Ns1) by FUNCT_2: 63;

      then ( rng q2) c= ( rng s2) by VALUED_0: 21;

      then

       A22: ( rng q2) c= Y by A20, XBOOLE_1: 1;

      then ( rng q2) c= ( dom f) by A3, XBOOLE_1: 1;

      then ( rng q2) c= (( dom f) /\ Y) by A22, XBOOLE_1: 19;

      then

       A23: ( rng q2) c= ( dom (f | Y)) by RELAT_1: 61;

       A24:

      now

        let p be Real such that

         A25: 0 < p;

        consider k be Nat such that

         A26: (p " ) < k by SEQ_4: 3;

        take k;

        let m be Nat;

        

         A27: m in NAT by ORDINAL1:def 12;

        assume k <= m;

        then (k + 1) <= (m + 1) by XREAL_1: 6;

        then (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

        then

         A28: ||.((s1 . m) - (s2 . m)).|| < (1 / (k + 1)) by A11, XXREAL_0: 2, A27;

        k < (k + 1) by NAT_1: 13;

        then (p " ) < (k + 1) by A26, XXREAL_0: 2;

        then (1 / (k + 1)) < (1 / (p " )) by A25, XREAL_1: 76;

        then

         A29: (1 / (k + 1)) < p by XCMPLX_1: 216;

         ||.(((s1 - s2) . m) - ( 0. S)).|| = ||.(((s1 . m) - (s2 . m)) - ( 0. S)).|| by NORMSP_1:def 3

        .= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1: 13;

        hence ||.(((s1 - s2) . m) - ( 0. S)).|| < p by A29, A28, XXREAL_0: 2;

      end;

      then

       A30: (s1 - s2) is convergent by NORMSP_1:def 6;

      then

       A31: ((s1 - s2) * Ns1) is convergent by LOPBAN_3: 7;

      then

       A32: q2 is convergent by A15, NORMSP_1: 20;

      ( rng q1) c= ( rng s1) by A14, VALUED_0: 21;

      then

       A33: ( rng q1) c= Y by A13, XBOOLE_1: 1;

      then ( rng q1) c= ( dom f) by A3, XBOOLE_1: 1;

      then ( rng q1) c= (( dom f) /\ Y) by A33, XBOOLE_1: 19;

      then

       A34: ( rng q1) c= ( dom (f | Y)) by RELAT_1: 61;

      then

       A35: ((f | Y) /. ( lim q1)) = ( lim ((f | Y) /* q1)) by A15, A18, NFCONT_1:def 5;

      

       A36: ((f | Y) /* q1) is convergent by A15, A18, A34, NFCONT_1:def 5;

      ( lim (s1 - s2)) = ( 0. S) by A24, A30, NORMSP_1:def 7;

      then ( lim ((s1 - s2) * Ns1)) = ( 0. S) by A30, LOPBAN_3: 8;

      

      then

       A37: ( lim q2) = (( lim q1) - ( 0. S)) by A15, A31, NORMSP_1: 26

      .= ( lim q1) by RLVECT_1: 13;

      then

       A38: ((f | Y) /* q2) is convergent by A18, A32, A23, NFCONT_1:def 5;

      then

       A39: (((f | Y) /* q1) - ((f | Y) /* q2)) is convergent by A36, NORMSP_1: 20;

      ((f | Y) /. ( lim q1)) = ( lim ((f | Y) /* q2)) by A18, A32, A37, A23, NFCONT_1:def 5;

      

      then

       A40: ( lim (((f | Y) /* q1) - ((f | Y) /* q2))) = (((f | Y) /. ( lim q1)) - ((f | Y) /. ( lim q1))) by A36, A35, A38, NORMSP_1: 26

      .= ( 0. T) by RLVECT_1: 15;

      now

        let n;

        reconsider r as Real;

        consider k be Nat such that

         A41: for m be Nat st k <= m holds ||.(((((f | Y) /* q1) - ((f | Y) /* q2)) . m) - ( 0. T)).|| < r by A4, A39, A40, NORMSP_1:def 7;

        

         A42: k in NAT by ORDINAL1:def 12;

        

         A43: (q1 . k) in ( rng q1) by NFCONT_1: 6;

        

         A44: (q2 . k) in ( rng q2) by NFCONT_1: 6;

         ||.(((((f | Y) /* q1) - ((f | Y) /* q2)) . k) - ( 0. T)).|| = ||.((((f | Y) /* q1) - ((f | Y) /* q2)) . k).|| by RLVECT_1: 13

        .= ||.((((f | Y) /* q1) . k) - (((f | Y) /* q2) . k)).|| by NORMSP_1:def 3

        .= ||.(((f | Y) /. (q1 . k)) - (((f | Y) /* q2) . k)).|| by A34, FUNCT_2: 109, A42

        .= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. (q2 . k))).|| by A23, FUNCT_2: 109, A42

        .= ||.((f /. (q1 . k)) - ((f | Y) /. (q2 . k))).|| by A34, A43, PARTFUN2: 15

        .= ||.((f /. (q1 . k)) - (f /. (q2 . k))).|| by A23, A44, PARTFUN2: 15

        .= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A17, A21, FUNCT_2: 15, A42

        .= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2: 15, A42;

        hence contradiction by A11, A41;

      end;

      hence contradiction;

    end;

    theorem :: NFCONT_2:11

    Y c= ( dom f) & Y is compact & f is_uniformly_continuous_on Y implies (f .: Y) is compact by Th7, NFCONT_1: 32;

    theorem :: NFCONT_2:12

    for f be PartFunc of the carrier of S, REAL holds for Y st Y <> {} & Y c= ( dom f) & Y is compact & f is_uniformly_continuous_on Y holds ex x1, x2 st x1 in Y & x2 in Y & (f /. x1) = ( upper_bound (f .: Y)) & (f /. x2) = ( lower_bound (f .: Y)) by Th8, NFCONT_1: 37;

    theorem :: NFCONT_2:13

    X c= ( dom f) & (f | X) is constant implies f is_uniformly_continuous_on X by Th9, NFCONT_1: 43;

    begin

    definition

      let M be non empty NORMSTR;

      let f be Function of M, M;

      :: NFCONT_2:def3

      attr f is contraction means

      : Def3: ex L be Real st 0 < L & L < 1 & for x,y be Point of M holds ||.((f . x) - (f . y)).|| <= (L * ||.(x - y).||);

    end

    registration

      let M be RealNormSpace;

      cluster contraction for Function of M, M;

      existence

      proof

        set x = the Point of M;

        reconsider f = (the carrier of M --> x) as Function of the carrier of M, the carrier of M;

        reconsider jd = (1 / 2) as Real;

        take f, jd;

        thus 0 < jd & jd < 1;

        let z,y be Point of M;

        (f . z) = x & (f . y) = x by FUNCOP_1: 7;

        then

         A1: ||.((f . z) - (f . y)).|| = 0 by NORMSP_1: 6;

        thus thesis by A1;

      end;

    end

    definition

      let M be RealNormSpace;

      mode Contraction of M is contraction Function of M, M;

    end

    

     Lm1: (for X be RealNormSpace holds for x,y be Point of X holds ||.(x - y).|| = 0 iff x = y) & (for X be RealNormSpace holds for x,y be Point of X holds ||.(x - y).|| <> 0 iff x <> y) & (for X be RealNormSpace holds for x,y be Point of X holds ||.(x - y).|| > 0 iff x <> y) & (for X be RealNormSpace holds for x,y be Point of X holds ||.(x - y).|| = ||.(y - x).||) & (for X be RealNormSpace holds for x,y,z be Point of X holds for e be Real st e > 0 holds (( ||.(x - z).|| < (e / 2) & ||.(z - y).|| < (e / 2)) implies ||.(x - y).|| < e)) & (for X be RealNormSpace holds for x,y,z be Point of X holds for e be Real st e > 0 holds (( ||.(x - z).|| < (e / 2) & ||.(y - z).|| < (e / 2)) implies ||.(x - y).|| < e)) & (for X be RealNormSpace holds for x be Point of X st (for e be Real st e > 0 holds ||.x.|| < e) holds x = ( 0. X)) & for X be RealNormSpace holds for x,y be Point of X st (for e be Real st e > 0 holds ||.(x - y).|| < e) holds x = y

    proof

      

       A1: for X be RealNormSpace holds for x,y,z be Point of X holds for e be Real st e > 0 holds ( ||.(x - z).|| < (e / 2) & ||.(z - y).|| < (e / 2) implies ||.(x - y).|| < e)

      proof

        let X be RealNormSpace;

        let x,y,z be Point of X;

        let e be Real such that e > 0 ;

        assume ||.(x - z).|| < (e / 2) & ||.(z - y).|| < (e / 2);

        then ( ||.(x - z).|| + ||.(z - y).||) < ((e / 2) + (e / 2)) by XREAL_1: 8;

        then ( ||.(x - y).|| + ( ||.(x - z).|| + ||.(z - y).||)) < (( ||.(x - z).|| + ||.(z - y).||) + e) by NORMSP_1: 10, XREAL_1: 8;

        then (( ||.(x - y).|| + ( ||.(x - z).|| + ||.(z - y).||)) + ( - ( ||.(x - z).|| + ||.(z - y).||))) < ((e + ( ||.(x - z).|| + ||.(z - y).||)) + ( - ( ||.(x - z).|| + ||.(z - y).||))) by XREAL_1: 8;

        hence thesis;

      end;

      

       A2: for X be RealNormSpace holds for x,y,z be Point of X holds for e be Real st e > 0 holds ( ||.(x - z).|| < (e / 2) & ||.(y - z).|| < (e / 2) implies ||.(x - y).|| < e)

      proof

        let X be RealNormSpace;

        let x,y,z be Point of X;

        let e be Real such that

         A3: e > 0 ;

        assume that

         A4: ||.(x - z).|| < (e / 2) and

         A5: ||.(y - z).|| < (e / 2);

         ||.( - (y - z)).|| < (e / 2) by A5, NORMSP_1: 2;

        then ||.(z - y).|| < (e / 2) by RLVECT_1: 33;

        hence thesis by A1, A3, A4;

      end;

      

       A6: for X be RealNormSpace holds for x,y be Point of X holds ||.(x - y).|| > 0 iff x <> y

      proof

        let X be RealNormSpace;

        let x,y be Point of X;

         0 < ||.(x - y).|| implies (x - y) <> ( 0. X) by NORMSP_0:def 6;

        hence 0 < ||.(x - y).|| implies x <> y by RLVECT_1: 15;

        now

          assume x <> y;

          then 0 <> ||.(x - y).|| by NORMSP_1: 11;

          hence 0 < ||.(x - y).||;

        end;

        hence thesis;

      end;

      

       A7: for X be RealNormSpace holds for x,y be Point of X holds ||.(x - y).|| = ||.(y - x).||

      proof

        let X be RealNormSpace;

        let x,y be Point of X;

        

        thus ||.(x - y).|| = ||.( - (x - y)).|| by NORMSP_1: 2

        .= ||.(y - x).|| by RLVECT_1: 33;

      end;

      

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

      proof

        let X be RealNormSpace;

        let x be Point of X such that

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

        now

          assume x <> ( 0. X);

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

          then 0 < ||.x.||;

          hence contradiction by A9;

        end;

        hence thesis;

      end;

      thus thesis by A6, A7, A1, A2, A8;

    end;

    

     Lm2: 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 & K < 1 and

       A2: 0 < e;

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

      consider rseq be Real_Sequence such that

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

      

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

      

       A5: ( lim rseq) = 0 by A1, A3, SERIES_1: 1;

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

      .= 0 by A5;

      then

      consider n be Nat such that

       A6: for m be Nat st n <= m holds |.(((L (#) rseq) . m) - 0 ).| < e by A2, A4, SEQ_2:def 7;

       |.(((L (#) rseq) . n) - 0 ).| < e by A6;

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

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

      hence thesis;

    end;

    theorem :: NFCONT_2:14

    

     Th14: for X be RealBanachSpace holds for f be Function of X, X st f is Contraction of X 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;

      set x0 = the Element of X;

      let f be Function of X, X;

      assume f is Contraction of X;

      then

      consider K be Real such that

       A1: 0 < K and

       A2: K < 1 and

       A3: for x,y be Point of X holds ||.((f . x) - (f . y)).|| <= (K * ||.(x - y).||) by Def3;

      deffunc G( set, set) = (f . $2);

      consider g be Function such that

       A4: ( dom g) = NAT & (g . 0 ) = x0 & for n be Nat holds (g . (n + 1)) = G(n,.) from NAT_1:sch 11;

      defpred P[ Nat] means (g . $1) in the carrier of X;

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat such that

         A6: P[k];

        (g . (k + 1)) = (f . (g . k)) by A4;

        hence thesis by A6, FUNCT_2: 5;

      end;

      

       A7: P[ 0 ] by A4;

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

      then for n be object st n in NAT holds (g . n) in the carrier of X;

      then

      reconsider g as sequence of X by A4, FUNCT_2: 3;

       A8:

      now

        let n be Nat;

         ||.(((g ^\ 1) . n) - (f . ( lim g))).|| = ||.((g . (n + 1)) - (f . ( lim g))).|| by NAT_1:def 3

        .= ||.((f . (g . n)) - (f . ( lim g))).|| by A4;

        hence ||.(((g ^\ 1) . n) - (f . ( lim g))).|| <= (K * ||.((g . n) - ( lim g)).||) by A3;

      end;

      

       A9: for n be Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K to_power n))

      proof

        defpred P[ Nat] means ||.((g . ($1 + 1)) - (g . $1)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K to_power $1));

        

         A10: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume P[k];

          then

           A11: (K * ||.((g . (k + 1)) - (g . k)).||) <= (K * ( ||.((g . 1) - (g . 0 )).|| * (K to_power k))) by A1, XREAL_1: 64;

           ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= (K * ||.((g . (k + 1)) - (g . k)).||) by A3;

          then ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K * (K to_power k))) by A11, XXREAL_0: 2;

          then

           A12: ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power 1) * (K to_power k))) by POWER: 25;

          (g . (k + 1)) = (f . (g . k)) by A4;

          then ||.((g . ((k + 1) + 1)) - (g . (k + 1))).|| = ||.((f . (g . (k + 1))) - (f . (g . k))).|| by A4;

          hence thesis by A1, A12, POWER: 27;

        end;

         ||.((g . ( 0 + 1)) - (g . 0 )).|| = ( ||.((g . 1) - (g . 0 )).|| * 1)

        .= ( ||.((g . 1) - (g . 0 )).|| * (K to_power 0 )) by POWER: 24;

        then

         A13: P[ 0 ];

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

        hence thesis;

      end;

      

       A14: for k,n be Nat holds ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)))

      proof

        defpred P[ Nat] means for n be Nat holds ||.((g . (n + $1)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + $1))) / (1 - K)));

         A15:

        now

          let k be Nat such that

           A16: P[k];

          now

            let n be Nat;

            (1 - K) <> 0 by A2;

            

            then

             A17: (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k)))) = (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ((( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k))) * (1 - K)) / (1 - K))) by XCMPLX_1: 89

            .= (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (( ||.((g . 1) - (g . 0 )).|| * ((K to_power (n + k)) * (1 - K))) / (1 - K)))

            .= (( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ( ||.((g . 1) - (g . 0 )).|| * (((K to_power (n + k)) * (1 - K)) / (1 - K)))) by XCMPLX_1: 74

            .= ( ||.((g . 1) - (g . 0 )).|| * ((((K to_power n) - (K to_power (n + k))) / (1 - K)) + (((K to_power (n + k)) * (1 - K)) / (1 - K))))

            .= ( ||.((g . 1) - (g . 0 )).|| * ((((K to_power n) - (K to_power (n + k))) + ((K to_power (n + k)) * (1 - K))) / (1 - K))) by XCMPLX_1: 62

            .= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K * (K to_power (n + k)))) / (1 - K)))

            .= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - ((K to_power 1) * (K to_power (n + k)))) / (1 - K))) by POWER: 25

            .= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power ((n + k) + 1))) / (1 - K))) by A1, POWER: 27;

             ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) & ||.((g . ((n + k) + 1)) - (g . (n + k))).|| <= ( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k))) by A9, A16;

            then ||.((g . (n + (k + 1))) - (g . n)).|| <= ( ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).||) & ( ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).||) <= (( ||.((g . 1) - (g . 0 )).|| * (K to_power (n + k))) + ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)))) by NORMSP_1: 10, XREAL_1: 7;

            hence ||.((g . (n + (k + 1))) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + (k + 1)))) / (1 - K))) by A17, XXREAL_0: 2;

          end;

          hence P[(k + 1)];

        end;

        now

          let n be Nat;

           ||.((g . (n + 0 )) - (g . n)).|| = ||.( 0. X).|| by RLVECT_1: 15

          .= 0 by NORMSP_1: 1;

          hence ||.((g . (n + 0 )) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + 0 ))) / (1 - K)));

        end;

        then

         A18: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A18, A15);

        hence thesis;

      end;

      

       A19: for k,n be Nat holds ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K)))

      proof

        let k be Nat;

        now

          let n be Nat;

          (K to_power (n + k)) > 0 by A1, POWER: 34;

          then

           A20: ((K to_power n) - (K to_power (n + k))) <= ((K to_power n) - 0 ) by XREAL_1: 13;

          (1 - K) > (1 - 1) by A2, XREAL_1: 15;

          then (((K to_power n) - (K to_power (n + k))) / (1 - K)) <= ((K to_power n) / (1 - K)) by A20, XREAL_1: 72;

          then

           A21: ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by XREAL_1: 64;

           ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) by A14;

          hence ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by A21, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      now

        let e be Real such that

         A22: e > 0 ;

        (e / 2) > 0 by A22, XREAL_1: 215;

        then

        consider n be Nat such that

         A23: |.(( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)).| < (e / 2) by A1, A2, Lm2;

        reconsider nn = (n + 1) as Nat;

        take nn;

        (( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)) <= |.(( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)).| by ABSVALUE: 4;

        then (( ||.((g . 1) - (g . 0 )).|| / (1 - K)) * (K to_power n)) < (e / 2) by A23, XXREAL_0: 2;

        then

         A24: ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) < (e / 2) by XCMPLX_1: 75;

        now

          let m,l be Nat such that

           A25: nn <= m and

           A26: nn <= l;

          n < m by A25, NAT_1: 13;

          then

          consider k1 be Nat such that

           A27: (n + k1) = m by NAT_1: 10;

          n < l by A26, NAT_1: 13;

          then

          consider k2 be Nat such that

           A28: (n + k2) = l by NAT_1: 10;

          reconsider k2 as Nat;

           ||.((g . (n + k2)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by A19;

          then

           A29: ||.((g . l) - (g . n)).|| < (e / 2) by A24, A28, XXREAL_0: 2;

          reconsider k1 as Nat;

           ||.((g . (n + k1)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K))) by A19;

          then ||.((g . m) - (g . n)).|| < (e / 2) by A24, A27, XXREAL_0: 2;

          hence ||.((g . l) - (g . m)).|| < e by A22, A29, Lm1;

        end;

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

      end;

      then g is Cauchy_sequence_by_Norm by RSSPACE3: 8;

      then

       A30: g is convergent by LOPBAN_1:def 15;

      then

       A31: (K (#) ||.(g - ( lim g)).||) is convergent by NORMSP_1: 24, SEQ_2: 7;

      

       A32: ( lim (K (#) ||.(g - ( lim g)).||)) = (K * ( lim ||.(g - ( lim g)).||)) by A30, NORMSP_1: 24, SEQ_2: 8

      .= (K * 0 ) by A30, NORMSP_1: 24

      .= 0 ;

      

       A33: for e be Real st e > 0 holds ex n be Nat st for m be Nat st n <= m holds ||.(((g ^\ 1) . m) - (f . ( lim g))).|| < e

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider n be Nat such that

         A34: for m be Nat st n <= m holds |.(((K (#) ||.(g - ( lim g)).||) . m) - 0 ).| < e by A31, A32, SEQ_2:def 7;

        take n;

        now

          let m be Nat;

          assume n <= m;

          then |.(((K (#) ||.(g - ( lim g)).||) . m) - 0 ).| < e by A34;

          then |.(K * ( ||.(g - ( lim g)).|| . m)).| < e by SEQ_1: 9;

          then |.(K * ||.((g - ( lim g)) . m).||).| < e by NORMSP_0:def 4;

          then

           A35: |.(K * ||.((g . m) - ( lim g)).||).| < e by NORMSP_1:def 4;

          (K * ||.((g . m) - ( lim g)).||) <= |.(K * ||.((g . m) - ( lim g)).||).| by ABSVALUE: 4;

          then

           A36: (K * ||.((g . m) - ( lim g)).||) < e by A35, XXREAL_0: 2;

           ||.(((g ^\ 1) . m) - (f . ( lim g))).|| <= (K * ||.((g . m) - ( lim g)).||) by A8;

          hence ||.(((g ^\ 1) . m) - (f . ( lim g))).|| < e by A36, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      take xp = ( lim g);

      

       A37: (g ^\ 1) is convergent & ( lim (g ^\ 1)) = ( lim g) by A30, LOPBAN_3: 9;

      then

       A38: ( lim g) = (f . ( lim g)) by A33, NORMSP_1:def 7;

      now

        let x be Point of X such that

         A39: (f . x) = x;

        

         A40: for k be Nat holds ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power k))

        proof

          defpred P[ Nat] means ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power $1));

          

           A41: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume P[k];

            then

             A42: (K * ||.(x - xp).||) <= (K * ( ||.(x - xp).|| * (K to_power k))) by A1, XREAL_1: 64;

             ||.((f . x) - (f . xp)).|| <= (K * ||.(x - xp).||) by A3;

            then ||.((f . x) - (f . xp)).|| <= ( ||.(x - xp).|| * (K * (K to_power k))) by A42, XXREAL_0: 2;

            then ||.((f . x) - (f . xp)).|| <= ( ||.(x - xp).|| * ((K to_power 1) * (K to_power k))) by POWER: 25;

            hence thesis by A1, A38, A39, POWER: 27;

          end;

           ||.(x - xp).|| = ( ||.(x - xp).|| * 1)

          .= ( ||.(x - xp).|| * (K to_power 0 )) by POWER: 24;

          then

           A43: P[ 0 ];

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

          hence thesis;

        end;

        for e be Real st 0 < e holds ||.(x - xp).|| < e

        proof

          let e be Real;

          assume 0 < e;

          then

          consider n be Nat such that

           A44: |.( ||.(x - xp).|| * (K to_power n)).| < e by A1, A2, Lm2;

          ( ||.(x - xp).|| * (K to_power n)) <= |.( ||.(x - xp).|| * (K to_power n)).| by ABSVALUE: 4;

          then

           A45: ( ||.(x - xp).|| * (K to_power n)) < e by A44, XXREAL_0: 2;

           ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power n)) by A40;

          hence thesis by A45, XXREAL_0: 2;

        end;

        hence x = xp by Lm1;

      end;

      hence thesis by A37, A33, NORMSP_1:def 7;

    end;

    theorem :: NFCONT_2:15

    for X be RealBanachSpace holds for f be Function of X, X st ex n0 be Nat st ( iter (f,n0)) is Contraction of X 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;

      given n0 be Nat such that

       A1: ( iter (f,n0)) is Contraction of X;

      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, Th14;

       A4:

      now

        let x be Point of X such that

         A5: (f . x) = x;

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

        proof

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

           A6:

          now

            let n be Nat such that

             A7: P[n];

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

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

            hence P[(n + 1)];

          end;

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

          .= x;

          then

           A8: P[ 0 ];

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

          hence thesis;

        end;

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

        hence xp = x by A3;

      end;

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

      then (f . xp) = xp by A3;

      hence thesis by A4;

    end;

    theorem :: NFCONT_2:16

    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 by Lm2;