ncfcont2.miz



    begin

    reserve X,X1 for set,

r,s for Real,

z for Complex,

RNS for RealNormSpace,

CNS,CNS1,CNS2 for ComplexNormSpace;

    definition

      let X be set;

      let CNS1,CNS2 be ComplexNormSpace;

      let f be PartFunc of CNS1, CNS2;

      :: NCFCONT2: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 be Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r;

    end

    definition

      let X be set;

      let RNS be RealNormSpace;

      let CNS be ComplexNormSpace;

      let f be PartFunc of CNS, RNS;

      :: NCFCONT2: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 be Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r;

    end

    definition

      let X be set;

      let RNS be RealNormSpace;

      let CNS be ComplexNormSpace;

      let f be PartFunc of RNS, CNS;

      :: NCFCONT2:def3

      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 be Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r;

    end

    definition

      let X be set;

      let CNS be ComplexNormSpace;

      let f be PartFunc of the carrier of CNS, COMPLEX ;

      :: NCFCONT2:def4

      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 be Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds |.((f /. x1) - (f /. x2)).| < r;

    end

    definition

      let X be set;

      let CNS be ComplexNormSpace;

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

      :: NCFCONT2:def5

      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 be Point of CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds |.((f /. x1) - (f /. x2)).| < r;

    end

    definition

      let X be set;

      let RNS be RealNormSpace;

      let f be PartFunc of the carrier of RNS, COMPLEX ;

      :: NCFCONT2:def6

      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 be Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds |.((f /. x1) - (f /. x2)).| < r;

    end

    theorem :: NCFCONT2:1

    

     Th1: for f be PartFunc of CNS1, CNS2 st f is_uniformly_continuous_on X & X1 c= X holds f is_uniformly_continuous_on X1

    proof

      let f be PartFunc of CNS1, CNS2;

      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 be Point of CNS1 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 be Point of CNS1;

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

      hence thesis by A2, A4;

    end;

    theorem :: NCFCONT2:2

    

     Th2: for f be PartFunc of CNS, RNS st f is_uniformly_continuous_on X & X1 c= X holds f is_uniformly_continuous_on X1

    proof

      let f be PartFunc of CNS, RNS;

      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 be Point of CNS 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 be Point of CNS;

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

      hence thesis by A2, A4;

    end;

    theorem :: NCFCONT2:3

    

     Th3: for f be PartFunc of RNS, CNS st f is_uniformly_continuous_on X & X1 c= X holds f is_uniformly_continuous_on X1

    proof

      let f be PartFunc of RNS, CNS;

      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 be Point of RNS 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 be Point of RNS;

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

      hence thesis by A2, A4;

    end;

    theorem :: NCFCONT2:4

    for f1,f2 be PartFunc of CNS1, CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds (f1 + f2) is_uniformly_continuous_on (X /\ X1)

    proof

      let f1,f2 be PartFunc of CNS1, CNS2;

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

      then

      consider s such that

       A8: 0 < s and

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

      consider g be Real such that

       A10: 0 < g and

       A11: for x1,x2 be Point of CNS1 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 be Point of CNS1;

      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 CLVECT_1:def 13;

       ||.(((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 :: NCFCONT2:5

    for f1,f2 be PartFunc of CNS, RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds (f1 + f2) is_uniformly_continuous_on (X /\ X1)

    proof

      let f1,f2 be PartFunc of CNS, RNS;

      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, Th2, XBOOLE_1: 17;

      then

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

      

       A5: f1 is_uniformly_continuous_on (X /\ X1) by A1, Th2, 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);

      then

      consider s such that

       A8: 0 < s and

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

      consider g be Real such that

       A10: 0 < g and

       A11: for x1,x2 be Point of CNS 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 be Point of CNS;

      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 :: NCFCONT2:6

    for f1,f2 be PartFunc of RNS, CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds (f1 + f2) is_uniformly_continuous_on (X /\ X1)

    proof

      let f1,f2 be PartFunc of RNS, CNS;

      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, Th3, XBOOLE_1: 17;

      then

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

      

       A5: f1 is_uniformly_continuous_on (X /\ X1) by A1, Th3, 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);

      then

      consider s such that

       A8: 0 < s and

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

      consider g be Real such that

       A10: 0 < g and

       A11: for x1,x2 be Point of RNS 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 be Point of RNS;

      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 CLVECT_1:def 13;

       ||.(((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 :: NCFCONT2:7

    for f1,f2 be PartFunc of CNS1, CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds (f1 - f2) is_uniformly_continuous_on (X /\ X1)

    proof

      let f1,f2 be PartFunc of CNS1, CNS2;

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

      then

      consider s such that

       A8: 0 < s and

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

      consider g be Real such that

       A10: 0 < g and

       A11: for x1,x2 be Point of CNS1 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 be Point of CNS1;

      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 CLVECT_1: 104;

       ||.(((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 :: NCFCONT2:8

    for f1,f2 be PartFunc of CNS, RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds (f1 - f2) is_uniformly_continuous_on (X /\ X1)

    proof

      let f1,f2 be PartFunc of CNS, RNS;

      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, Th2, XBOOLE_1: 17;

      then

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

      

       A5: f1 is_uniformly_continuous_on (X /\ X1) by A1, Th2, 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);

      then

      consider s such that

       A8: 0 < s and

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

      consider g be Real such that

       A10: 0 < g and

       A11: for x1,x2 be Point of CNS 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 be Point of CNS;

      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 :: NCFCONT2:9

    for f1,f2 be PartFunc of RNS, CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds (f1 - f2) is_uniformly_continuous_on (X /\ X1)

    proof

      let f1,f2 be PartFunc of RNS, CNS;

      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, Th3, XBOOLE_1: 17;

      then

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

      

       A5: f1 is_uniformly_continuous_on (X /\ X1) by A1, Th3, 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);

      then

      consider s such that

       A8: 0 < s and

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

      consider g be Real such that

       A10: 0 < g and

       A11: for x1,x2 be Point of RNS 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 be Point of RNS;

      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 CLVECT_1: 104;

       ||.(((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 :: NCFCONT2:10

    

     Th10: for f be PartFunc of CNS1, CNS2 st f is_uniformly_continuous_on X holds (z (#) f) is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS1, CNS2;

      assume

       A1: f is_uniformly_continuous_on X;

      then X c= ( dom f);

      hence

       A2: X c= ( dom (z (#) f)) by VFUNCT_2:def 2;

      now

        per cases ;

          suppose

           A3: z = 0 ;

          let r;

          assume

           A4: 0 < r;

          then

          consider s such that

           A5: 0 < s and for x1,x2 be Point of CNS1 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 be Point of CNS1;

          assume that

           A6: x1 in X and

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

           ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A6, VFUNCT_2:def 2

          .= ||.(( 0. CNS2) - ((z (#) f) /. x2)).|| by A3, CLVECT_1: 1

          .= ||.(( 0. CNS2) - (z * (f /. x2))).|| by A2, A7, VFUNCT_2:def 2

          .= ||.(( 0. CNS2) - ( 0. CNS2)).|| by A3, CLVECT_1: 1

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

          .= 0 by NORMSP_0:def 6;

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

        end;

          suppose

           A8: z <> 0 ;

          let r;

          

           A9: 0 < |.z.| by A8, COMPLEX1: 47;

          assume 0 < r;

          then 0 < (r / |.z.|) by A9;

          then

          consider s such that

           A10: 0 < s and

           A11: for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < (r / |.z.|) by A1;

          take s;

          thus 0 < s by A10;

          let x1,x2 be Point of CNS1;

          assume that

           A12: x1 in X and

           A13: x2 in X and

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

          

           A15: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A12, VFUNCT_2:def 2

          .= ||.((z * (f /. x1)) - (z * (f /. x2))).|| by A2, A13, VFUNCT_2:def 2

          .= ||.(z * ((f /. x1) - (f /. x2))).|| by CLVECT_1: 9

          .= ( |.z.| * ||.((f /. x1) - (f /. x2)).||) by CLVECT_1:def 13;

          ( |.z.| * ||.((f /. x1) - (f /. x2)).||) < ((r / |.z.|) * |.z.|) by A9, A11, A12, A13, A14, XREAL_1: 68;

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

        end;

      end;

      hence thesis;

    end;

    theorem :: NCFCONT2:11

    

     Th11: for f be PartFunc of CNS, RNS st f is_uniformly_continuous_on X holds (r (#) f) is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS, RNS;

      assume

       A1: f is_uniformly_continuous_on X;

      then X c= ( dom f);

      hence

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

      now

        per cases ;

          suppose

           A3: r = 0 ;

          let p be Real;

          assume

           A4: 0 < p;

          then

          consider s such that

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

          take s;

          thus 0 < s by A5;

          let x1,x2 be Point of CNS;

          assume that

           A6: x1 in X and

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

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

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

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

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

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

          .= 0 by NORMSP_0:def 6;

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

        end;

          suppose

           A8: r <> 0 ;

          let p be Real;

          

           A9: 0 < |.r.| by A8, COMPLEX1: 47;

          assume 0 < p;

          then 0 < (p / |.r.|) by A9;

          then

          consider s such that

           A10: 0 < s and

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

          take s;

          thus 0 < s by A10;

          let x1,x2 be Point of CNS;

          assume that

           A12: x1 in X and

           A13: x2 in X and

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

          

           A15: ||.(((r (#) f) /. x1) - ((r (#) f) /. x2)).|| = ||.((r * (f /. x1)) - ((r (#) f) /. x2)).|| by A2, A12, VFUNCT_1:def 4

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

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

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

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

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

        end;

      end;

      hence thesis;

    end;

    theorem :: NCFCONT2:12

    

     Th12: for f be PartFunc of RNS, CNS st f is_uniformly_continuous_on X holds (z (#) f) is_uniformly_continuous_on X

    proof

      let f be PartFunc of RNS, CNS;

      assume

       A1: f is_uniformly_continuous_on X;

      then X c= ( dom f);

      hence

       A2: X c= ( dom (z (#) f)) by VFUNCT_2:def 2;

      now

        per cases ;

          suppose

           A3: z = 0 ;

          let r;

          assume

           A4: 0 < r;

          then

          consider s such that

           A5: 0 < s and for x1,x2 be Point of RNS 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 be Point of RNS;

          assume that

           A6: x1 in X and

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

           ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A6, VFUNCT_2:def 2

          .= ||.(( 0. CNS) - ((z (#) f) /. x2)).|| by A3, CLVECT_1: 1

          .= ||.(( 0. CNS) - (z * (f /. x2))).|| by A2, A7, VFUNCT_2:def 2

          .= ||.(( 0. CNS) - ( 0. CNS)).|| by A3, CLVECT_1: 1

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

          .= 0 by NORMSP_0:def 6;

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

        end;

          suppose

           A8: z <> 0 ;

          let r;

          

           A9: 0 < |.z.| by A8, COMPLEX1: 47;

          assume 0 < r;

          then 0 < (r / |.z.|) by A9;

          then

          consider s such that

           A10: 0 < s and

           A11: for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < (r / |.z.|) by A1;

          take s;

          thus 0 < s by A10;

          let x1,x2 be Point of RNS;

          assume that

           A12: x1 in X and

           A13: x2 in X and

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

          

           A15: ||.(((z (#) f) /. x1) - ((z (#) f) /. x2)).|| = ||.((z * (f /. x1)) - ((z (#) f) /. x2)).|| by A2, A12, VFUNCT_2:def 2

          .= ||.((z * (f /. x1)) - (z * (f /. x2))).|| by A2, A13, VFUNCT_2:def 2

          .= ||.(z * ((f /. x1) - (f /. x2))).|| by CLVECT_1: 9

          .= ( |.z.| * ||.((f /. x1) - (f /. x2)).||) by CLVECT_1:def 13;

          ( |.z.| * ||.((f /. x1) - (f /. x2)).||) < ((r / |.z.|) * |.z.|) by A9, A11, A12, A13, A14, XREAL_1: 68;

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

        end;

      end;

      hence thesis;

    end;

    theorem :: NCFCONT2:13

    for f be PartFunc of CNS1, CNS2 st f is_uniformly_continuous_on X holds ( - f) is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS1, CNS2;

      

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

      assume f is_uniformly_continuous_on X;

      hence thesis by A1, Th10;

    end;

    theorem :: NCFCONT2:14

    for f be PartFunc of CNS, RNS st f is_uniformly_continuous_on X holds ( - f) is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS, RNS;

      

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

      assume f is_uniformly_continuous_on X;

      hence thesis by A1, Th11;

    end;

    theorem :: NCFCONT2:15

    for f be PartFunc of RNS, CNS st f is_uniformly_continuous_on X holds ( - f) is_uniformly_continuous_on X

    proof

      let f be PartFunc of RNS, CNS;

      

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

      assume f is_uniformly_continuous_on X;

      hence thesis by A1, Th12;

    end;

    theorem :: NCFCONT2:16

    for f be PartFunc of CNS1, CNS2 st f is_uniformly_continuous_on X holds ||.f.|| is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS1, CNS2;

      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 be Point of CNS1 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 be Point of CNS1;

      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 CLVECT_1: 110;

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

      hence thesis by A8, XXREAL_0: 2;

    end;

    theorem :: NCFCONT2:17

    for f be PartFunc of CNS, RNS st f is_uniformly_continuous_on X holds ||.f.|| is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS, RNS;

      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 be Point of CNS 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 be Point of CNS;

      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 :: NCFCONT2:18

    for f be PartFunc of RNS, CNS st f is_uniformly_continuous_on X holds ||.f.|| is_uniformly_continuous_on X

    proof

      let f be PartFunc of RNS, CNS;

      assume

       A1: f is_uniformly_continuous_on X;

      then X c= ( dom f);

      then

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

      for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds |.(( ||.f.|| /. x1) - ( ||.f.|| /. x2)).| < r

      proof

        let r be Real;

        assume 0 < r;

        then

        consider s be Real such that

         A3: 0 < s and

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

        reconsider s as Real;

        take s;

        thus 0 < s by A3;

        let x1,x2 be Point of RNS;

        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 CLVECT_1: 110;

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

        hence thesis by A8, XXREAL_0: 2;

      end;

      hence thesis by A2, NFCONT_2:def 2;

    end;

    theorem :: NCFCONT2:19

    

     Th19: for f be PartFunc of CNS1, CNS2 st f is_uniformly_continuous_on X holds f is_continuous_on X

    proof

      let f be PartFunc of CNS1, CNS2;

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0 be Point of CNS1;

        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 be Point of CNS1 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 be Point of CNS1;

        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, NCFCONT1: 44;

    end;

    theorem :: NCFCONT2:20

    

     Th20: for f be PartFunc of CNS, RNS st f is_uniformly_continuous_on X holds f is_continuous_on X

    proof

      let f be PartFunc of CNS, RNS;

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0 be Point of CNS;

        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 be Point of CNS 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 be Point of CNS;

        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, NCFCONT1: 45;

    end;

    theorem :: NCFCONT2:21

    

     Th21: for f be PartFunc of RNS, CNS st f is_uniformly_continuous_on X holds f is_continuous_on X

    proof

      let f be PartFunc of RNS, CNS;

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0 be Point of RNS;

        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 be Point of RNS 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 be Point of RNS;

        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, NCFCONT1: 46;

    end;

    theorem :: NCFCONT2:22

    for f be PartFunc of the carrier of CNS, COMPLEX st f is_uniformly_continuous_on X holds f is_continuous_on X

    proof

      let f be PartFunc of the carrier of CNS, COMPLEX ;

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0 be Point of CNS;

        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 be Point of CNS 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 be Point of CNS;

        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, NCFCONT1: 47;

    end;

    theorem :: NCFCONT2:23

    

     Th23: for f be PartFunc of the carrier of CNS, REAL st f is_uniformly_continuous_on X holds f is_continuous_on X

    proof

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

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0 be Point of CNS;

        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 be Point of CNS 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 be Point of CNS;

        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, NCFCONT1: 48;

    end;

    theorem :: NCFCONT2:24

    for f be PartFunc of the carrier of RNS, COMPLEX st f is_uniformly_continuous_on X holds f is_continuous_on X

    proof

      let f be PartFunc of the carrier of RNS, COMPLEX ;

      assume

       A1: f is_uniformly_continuous_on X;

       A2:

      now

        let x0 be Point of RNS;

        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 be Point of RNS 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 be Point of RNS;

        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, NCFCONT1: 49;

    end;

    theorem :: NCFCONT2:25

    

     Th25: for f be PartFunc of CNS1, CNS2 st f is_Lipschitzian_on X holds f is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS1, CNS2;

      assume

       A1: f is_Lipschitzian_on X;

      hence X c= ( dom f) by NCFCONT1:def 17;

      consider r be Real such that

       A2: 0 < r and

       A3: for x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= (r * ||.(x1 - x2).||) by A1, NCFCONT1:def 17;

      let p be Real such that

       A4: 0 < p;

      take s = (p / r);

      thus 0 < s by A2, A4;

      let x1,x2 be Point of CNS1;

      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 :: NCFCONT2:26

    

     Th26: for f be PartFunc of CNS, RNS st f is_Lipschitzian_on X holds f is_uniformly_continuous_on X

    proof

      let f be PartFunc of CNS, RNS;

      assume

       A1: f is_Lipschitzian_on X;

      hence X c= ( dom f) by NCFCONT1:def 18;

      consider r be Real such that

       A2: 0 < r and

       A3: for x1,x2 be Point of CNS st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= (r * ||.(x1 - x2).||) by A1, NCFCONT1:def 18;

      let p be Real such that

       A4: 0 < p;

      take s = (p / r);

      thus 0 < s by A2, A4;

      let x1,x2 be Point of CNS;

      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 :: NCFCONT2:27

    

     Th27: for f be PartFunc of RNS, CNS st f is_Lipschitzian_on X holds f is_uniformly_continuous_on X

    proof

      let f be PartFunc of RNS, CNS;

      assume

       A1: f is_Lipschitzian_on X;

      hence X c= ( dom f) by NCFCONT1:def 19;

      consider r be Real such that

       A2: 0 < r and

       A3: for x1,x2 be Point of RNS st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= (r * ||.(x1 - x2).||) by A1, NCFCONT1:def 19;

      let p be Real such that

       A4: 0 < p;

      take s = (p / r);

      thus 0 < s by A2, A4;

      let x1,x2 be Point of RNS;

      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 :: NCFCONT2:28

    for f be PartFunc of CNS1, CNS2, Y be Subset of CNS1 st Y is compact & f is_continuous_on Y holds f is_uniformly_continuous_on Y

    proof

      let f be PartFunc of CNS1, CNS2;

      let Y be Subset of CNS1;

      assume that

       A1: Y is compact and

       A2: f is_continuous_on Y;

      

       A3: Y c= ( dom f) by A2, NCFCONT1:def 11;

      assume not thesis;

      then

      consider r such that

       A4: 0 < r and

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

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

       A6:

      now

        let n be Element of NAT ;

        consider x1 be Point of CNS1 such that

         A7: ex x2 be Point of CNS1 st x1 in Y & x2 in Y & ||.(x1 - x2).|| < (1 / (n + 1)) & not ||.((f /. x1) - (f /. x2)).|| < r by A5;

        take x1;

        thus P[n, x1] by A7;

      end;

      consider s1 be sequence of CNS1 such that

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

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

      

       A9: for n be Element of NAT holds ex x2 be Point of CNS1 st P1[n, x2] by A8;

      consider s2 be sequence of CNS1 such that

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

      

       A11: for n be Nat holds P1[n, (s2 . n)]

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A10;

      end;

      now

        let x be Point of CNS1;

        assume x in ( rng s1);

        then

        consider n be Nat such that

         A12: x = (s1 . n) by NCFCONT1: 7;

        n in NAT by ORDINAL1:def 12;

        hence x in Y by A8, A12;

      end;

      then for x be object st x in ( rng s1) holds x in Y;

      then

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

      then

      consider q1 be sequence of CNS1 such that

       A14: q1 is subsequence of s1 and

       A15: q1 is convergent and

       A16: ( lim q1) in Y by A1, NCFCONT1: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, NCFCONT1:def 11;

      now

        let x be object;

        assume x in ( rng s2);

        then

        consider n be Nat such that

         A19: x = (s2 . n) by NCFCONT1: 7;

        thus 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. CNS1) + (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;

        assume k <= m;

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

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

        then

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

        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

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

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

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

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

      end;

      then

       A29: (s1 - s2) is convergent by CLVECT_1:def 15;

      then

       A30: ((s1 - s2) * Ns1) is convergent by CLOPBAN3: 7;

      then

       A31: q2 is convergent by A15, CLVECT_1: 114;

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

      then

       A32: ( 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 A32, XBOOLE_1: 19;

      then

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

      then

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

      

       A35: ((f | Y) /* q1) is convergent by A15, A18, A33, NCFCONT1:def 5;

      ( lim (s1 - s2)) = ( 0. CNS1) by A24, A29, CLVECT_1:def 16;

      then ( lim ((s1 - s2) * Ns1)) = ( 0. CNS1) by A29, CLOPBAN3: 8;

      

      then

       A36: ( lim q2) = (( lim q1) - ( 0. CNS1)) by A15, A30, CLVECT_1: 120

      .= ( lim q1) by RLVECT_1: 13;

      then

       A37: ((f | Y) /* q2) is convergent by A18, A31, A23, NCFCONT1:def 5;

      then

       A38: (((f | Y) /* q1) - ((f | Y) /* q2)) is convergent by A35, CLVECT_1: 114;

      ((f | Y) /. ( lim q1)) = ( lim ((f | Y) /* q2)) by A18, A31, A36, A23, NCFCONT1:def 5;

      

      then

       A39: ( lim (((f | Y) /* q1) - ((f | Y) /* q2))) = (((f | Y) /. ( lim q1)) - ((f | Y) /. ( lim q1))) by A35, A34, A37, CLVECT_1: 120

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

      now

        let n be Element of NAT ;

        consider k be Nat such that

         A40: for m be Nat st k <= m holds ||.(((((f | Y) /* q1) - ((f | Y) /* q2)) . m) - ( 0. CNS2)).|| < r by A4, A38, A39, CLVECT_1:def 16;

        

         A41: k in NAT by ORDINAL1:def 12;

        

         A42: (q1 . k) in ( rng q1) by NCFCONT1: 7;

        

         A43: (q2 . k) in ( rng q2) by NCFCONT1: 7;

         ||.(((((f | Y) /* q1) - ((f | Y) /* q2)) . k) - ( 0. CNS2)).|| = ||.((((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 A33, FUNCT_2: 109, A41

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

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

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

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

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

        hence contradiction by A11, A40;

      end;

      hence contradiction;

    end;

    theorem :: NCFCONT2:29

    for f be PartFunc of CNS, RNS, Y be Subset of CNS st Y is compact & f is_continuous_on Y holds f is_uniformly_continuous_on Y

    proof

      let f be PartFunc of CNS, RNS;

      let Y be Subset of CNS;

      assume that

       A1: Y is compact and

       A2: f is_continuous_on Y;

      

       A3: Y c= ( dom f) by A2, NCFCONT1:def 12;

      assume not thesis;

      then

      consider r such that

       A4: 0 < r and

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

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

       A6:

      now

        let n be Element of NAT ;

        consider x1 be Point of CNS such that

         A7: ex x2 be Point of CNS st x1 in Y & x2 in Y & ||.(x1 - x2).|| < (1 / (n + 1)) & not ||.((f /. x1) - (f /. x2)).|| < r by A5;

        take x1;

        thus P[n, x1] by A7;

      end;

      consider s1 be sequence of CNS such that

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

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

      

       A9: for n be Element of NAT holds ex x2 be Point of CNS st P1[n, x2] by A8;

      consider s2 be sequence of CNS such that

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

      

       A11: for n be Nat holds P1[n, (s2 . n)]

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A10;

      end;

      now

        let x be Point of CNS;

        assume x in ( rng s1);

        then

        consider n be Nat such that

         A12: x = (s1 . n) by NCFCONT1: 7;

        n in NAT by ORDINAL1:def 12;

        hence x in Y by A8, A12;

      end;

      then for x be object st x in ( rng s1) holds x in Y;

      then

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

      then

      consider q1 be sequence of CNS such that

       A14: q1 is subsequence of s1 and

       A15: q1 is convergent and

       A16: ( lim q1) in Y by A1, NCFCONT1: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, NCFCONT1:def 12;

      now

        let x be object;

        assume x in ( rng s2);

        then

        consider n be Nat such that

         A19: x = (s2 . n) by NCFCONT1: 7;

        thus 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. CNS) + (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;

        assume k <= m;

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

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

        then

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

        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

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

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

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

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

      end;

      then

       A29: (s1 - s2) is convergent by CLVECT_1:def 15;

      then

       A30: ((s1 - s2) * Ns1) is convergent by CLOPBAN3: 7;

      then

       A31: q2 is convergent by A15, CLVECT_1: 114;

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

      then

       A32: ( 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 A32, XBOOLE_1: 19;

      then

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

      then

       A34: ((f | Y) /. ( lim q1)) = ( lim ((f | Y) /* q1)) by A15, A18, NCFCONT1:def 6;

      

       A35: ((f | Y) /* q1) is convergent by A15, A18, A33, NCFCONT1:def 6;

      ( lim (s1 - s2)) = ( 0. CNS) by A24, A29, CLVECT_1:def 16;

      then ( lim ((s1 - s2) * Ns1)) = ( 0. CNS) by A29, CLOPBAN3: 8;

      

      then

       A36: ( lim q2) = (( lim q1) - ( 0. CNS)) by A15, A30, CLVECT_1: 120

      .= ( lim q1) by RLVECT_1: 13;

      then

       A37: ((f | Y) /* q2) is convergent by A18, A31, A23, NCFCONT1:def 6;

      then

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

      ((f | Y) /. ( lim q1)) = ( lim ((f | Y) /* q2)) by A18, A31, A36, A23, NCFCONT1:def 6;

      

      then

       A39: ( lim (((f | Y) /* q1) - ((f | Y) /* q2))) = (((f | Y) /. ( lim q1)) - ((f | Y) /. ( lim q1))) by A35, A34, A37, NORMSP_1: 26

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

      now

        let n be Element of NAT ;

        consider k be Nat such that

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

        

         A41: k in NAT by ORDINAL1:def 12;

        

         A42: (q1 . k) in ( rng q1) by NCFCONT1: 7;

        

         A43: (q2 . k) in ( rng q2) by NCFCONT1: 7;

         ||.(((((f | Y) /* q1) - ((f | Y) /* q2)) . k) - ( 0. RNS)).|| = ||.((((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 A33, FUNCT_2: 109, A41

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

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

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

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

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

        hence contradiction by A11, A40;

      end;

      hence contradiction;

    end;

    theorem :: NCFCONT2:30

    for f be PartFunc of RNS, CNS, Y be Subset of RNS st Y is compact & f is_continuous_on Y holds f is_uniformly_continuous_on Y

    proof

      let f be PartFunc of RNS, CNS;

      let Y be Subset of RNS;

      assume that

       A1: Y is compact and

       A2: f is_continuous_on Y;

      

       A3: Y c= ( dom f) by A2, NCFCONT1:def 13;

      assume not thesis;

      then

      consider r such that

       A4: 0 < r and

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

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

       A6:

      now

        let n be Element of NAT ;

        consider x1 be Point of RNS such that

         A7: ex x2 be Point of RNS st x1 in Y & x2 in Y & ||.(x1 - x2).|| < (1 / (n + 1)) & not ||.((f /. x1) - (f /. x2)).|| < r by A5;

        take x1;

        thus P[n, x1] by A7;

      end;

      consider s1 be sequence of RNS such that

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

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

      

       A9: for n be Element of NAT holds ex x2 be Point of RNS st P1[n, x2] by A8;

      consider s2 be sequence of RNS such that

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

      

       A11: for n be Nat holds P1[n, (s2 . n)]

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A10;

      end;

      now

        let x be Point of RNS;

        assume x in ( rng s1);

        then

        consider n be Nat such that

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

        n in NAT by ORDINAL1:def 12;

        hence x in Y by A8, A12;

      end;

      then for x be object st x in ( rng s1) holds x in Y;

      then

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

      then

      consider q1 be sequence of RNS 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, NCFCONT1:def 13;

      now

        let x be object;

        assume x in ( rng s2);

        then

        consider n be Nat such that

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

        thus 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. RNS) + (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;

        assume k <= m;

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

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

        then

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

        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

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

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

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

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

      end;

      then

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

      then

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

      then

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

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

      then

       A32: ( 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 A32, XBOOLE_1: 19;

      then

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

      then

       A34: ((f | Y) /. ( lim q1)) = ( lim ((f | Y) /* q1)) by A15, A18, NCFCONT1:def 7;

      

       A35: ((f | Y) /* q1) is convergent by A15, A18, A33, NCFCONT1:def 7;

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

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

      

      then

       A36: ( lim q2) = (( lim q1) - ( 0. RNS)) by A15, A30, NORMSP_1: 26

      .= ( lim q1) by RLVECT_1: 13;

      then

       A37: ((f | Y) /* q2) is convergent by A18, A31, A23, NCFCONT1:def 7;

      then

       A38: (((f | Y) /* q1) - ((f | Y) /* q2)) is convergent by A35, CLVECT_1: 114;

      ((f | Y) /. ( lim q1)) = ( lim ((f | Y) /* q2)) by A18, A31, A36, A23, NCFCONT1:def 7;

      

      then

       A39: ( lim (((f | Y) /* q1) - ((f | Y) /* q2))) = (((f | Y) /. ( lim q1)) - ((f | Y) /. ( lim q1))) by A35, A34, A37, CLVECT_1: 120

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

      now

        let n be Element of NAT ;

        consider k be Nat such that

         A40: for m be Nat st k <= m holds ||.(((((f | Y) /* q1) - ((f | Y) /* q2)) . m) - ( 0. CNS)).|| < r by A4, A38, A39, CLVECT_1:def 16;

        

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

        

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

        

         A43: k in NAT by ORDINAL1:def 12;

         ||.(((((f | Y) /* q1) - ((f | Y) /* q2)) . k) - ( 0. CNS)).|| = ||.((((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 A33, FUNCT_2: 109, A43

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

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

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

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

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

        hence contradiction by A11, A40;

      end;

      hence contradiction;

    end;

    theorem :: NCFCONT2:31

    for f be PartFunc of CNS1, CNS2, Y be Subset of CNS1 st Y c= ( dom f) & Y is compact & f is_uniformly_continuous_on Y holds (f .: Y) is compact by Th19, NCFCONT1: 83;

    theorem :: NCFCONT2:32

    for f be PartFunc of CNS, RNS, Y be Subset of CNS st Y c= ( dom f) & Y is compact & f is_uniformly_continuous_on Y holds (f .: Y) is compact by Th20, NCFCONT1: 84;

    theorem :: NCFCONT2:33

    for f be PartFunc of RNS, CNS, Y be Subset of RNS st Y c= ( dom f) & Y is compact & f is_uniformly_continuous_on Y holds (f .: Y) is compact by Th21, NCFCONT1: 85;

    theorem :: NCFCONT2:34

    for f be PartFunc of the carrier of CNS, REAL , Y be Subset of CNS st Y <> {} & Y c= ( dom f) & Y is compact & f is_uniformly_continuous_on Y holds ex x1,x2 be Point of CNS st x1 in Y & x2 in Y & (f /. x1) = ( upper_bound (f .: Y)) & (f /. x2) = ( lower_bound (f .: Y)) by Th23, NCFCONT1: 96;

    theorem :: NCFCONT2:35

    for f be PartFunc of CNS1, CNS2 st X c= ( dom f) & (f | X) is constant holds f is_uniformly_continuous_on X by Th25, NCFCONT1: 112;

    theorem :: NCFCONT2:36

    for f be PartFunc of CNS, RNS st X c= ( dom f) & (f | X) is constant holds f is_uniformly_continuous_on X by Th26, NCFCONT1: 113;

    theorem :: NCFCONT2:37

    for f be PartFunc of RNS, CNS st X c= ( dom f) & (f | X) is constant holds f is_uniformly_continuous_on X by Th27, NCFCONT1: 114;

    begin

    definition

      let M be non empty CNORMSTR;

      let f be Function of M, M;

      :: NCFCONT2:def7

      attr f is contraction means

      : Def7: 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 ComplexBanachSpace;

      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 CLVECT_1: 107;

         ||.(z - y).|| >= 0 by CLVECT_1: 105;

        hence thesis by A1;

      end;

    end

    definition

      let M be ComplexBanachSpace;

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

    end

    theorem :: NCFCONT2:38

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

    proof

      let X be ComplexNormSpace;

      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 CLVECT_1: 112;

        hence 0 < ||.(x - y).|| by CLVECT_1: 105;

      end;

      hence thesis;

    end;

    theorem :: NCFCONT2:39

    for X be ComplexNormSpace, x,y be Point of X holds ||.(x - y).|| = ||.(y - x).||

    proof

      let X be ComplexNormSpace;

      let x,y be Point of X;

      

      thus ||.(x - y).|| = ||.( - (x - y)).|| by CLVECT_1: 103

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

    end;

    

     Lm1: for X be ComplexNormSpace, x,y,z be Point of X, e be Real holds ( ||.(x - z).|| < (e / 2) & ||.(z - y).|| < (e / 2) implies ||.(x - y).|| < e)

    proof

      let X be ComplexNormSpace;

      let x,y,z be Point of X;

      let e be Real;

      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 CLVECT_1: 111, 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;

    

     Lm2: for X be ComplexNormSpace, x,y,z be Point of X, e be Real holds ||.(x - z).|| < (e / 2) & ||.(y - z).|| < (e / 2) implies ||.(x - y).|| < e

    proof

      let X be ComplexNormSpace;

      let x,y,z be Point of X;

      let e be Real;

      assume that

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

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

       ||.( - (y - z)).|| < (e / 2) by A2, CLVECT_1: 103;

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

      hence thesis by A1, Lm1;

    end;

    

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

    proof

      let X be ComplexNormSpace;

      let x be Point of X such that

       A1: 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.|| by CLVECT_1: 105;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    

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

    proof

      let X be ComplexNormSpace;

      let x,y be Point of X;

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

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

      hence thesis by RLVECT_1: 21;

    end;

    theorem :: NCFCONT2:40

    

     Th40: for X be ComplexBanachSpace, 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 ComplexBanachSpace;

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

      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 Element of 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) + 1)) = (f . (g . (k + 1))) & (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 Element of 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 Element of 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 Element of 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))) + ((1 * (K to_power (n + k))) - (K * (K to_power (n + 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 CLVECT_1: 111, 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 Element of NAT ;

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

          .= 0 by CLVECT_1: 102;

          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 Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ( ||.((g . 1) - (g . 0 )).|| * ((K to_power n) / (1 - K)))

      proof

        let k be Element of NAT ;

        now

          let n be Element of NAT ;

          

           A20: 0 <= ||.((g . 1) - (g . 0 )).|| by CLVECT_1: 105;

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

          then

           A21: ((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 A21, XREAL_1: 72;

          then

           A22: ( ||.((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 A20, 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 A22, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      now

        let e be Real such that

         A23: e > 0 ;

        (e / 2) > 0 by A23;

        then

        consider n be Nat such that

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

        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 A24, XXREAL_0: 2;

        then

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

        now

          let m,l be Nat such that

           A26: nn <= m and

           A27: nn <= l;

          n < m by A26, NAT_1: 13;

          then

          consider k1 be Nat such that

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

          n < l by A27, NAT_1: 13;

          then

          consider k2 be Nat such that

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

          reconsider k2 as Nat;

          

           A30: n in NAT by ORDINAL1:def 12;

          

           A31: k2 in NAT by ORDINAL1:def 12;

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

          then

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

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

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

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

          hence ||.((g . l) - (g . m)).|| < e by A32, Lm2;

        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 CSSPACE3: 8;

      then

       A33: g is convergent by CLOPBAN1:def 13;

      then

       A34: (K (#) ||.(g - ( lim g)).||) is convergent by CLVECT_1: 118, SEQ_2: 7;

      

       A35: ( lim (K (#) ||.(g - ( lim g)).||)) = (K * ( lim ||.(g - ( lim g)).||)) by A33, CLVECT_1: 118, SEQ_2: 8

      .= (K * 0 ) by A33, CLVECT_1: 118

      .= 0 ;

      

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

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

        take n;

        now

          let m be Nat;

          

           A38: m in NAT by ORDINAL1:def 12;

          assume n <= m;

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

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

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

          then

           A39: |.(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

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

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

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

        end;

        hence thesis;

      end;

      take xp = ( lim g);

      

       A41: (g ^\ 1) is convergent & ( lim (g ^\ 1)) = ( lim g) by A33, CLOPBAN3: 9;

      then

       A42: ( lim g) = (f . ( lim g)) by A36, CLVECT_1:def 16;

      now

        let x be Point of X such that

         A43: (f . x) = x;

        

         A44: for k be Element of NAT holds ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power k))

        proof

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

          

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

          proof

            let k be Nat;

            assume P[k];

            then

             A46: (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 A46, 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, A42, A43, POWER: 27;

          end;

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

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

          then

           A47: P[ 0 ];

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

          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

           A48: |.( ||.(x - xp).|| * (K to_power n)).| < e by A1, A2, NFCONT_2: 16;

          

           A49: n in NAT by ORDINAL1:def 12;

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

          then

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

           ||.(x - xp).|| <= ( ||.(x - xp).|| * (K to_power n)) by A44, A49;

          hence thesis by A50, XXREAL_0: 2;

        end;

        hence x = xp by Lm4;

      end;

      hence thesis by A41, A36, CLVECT_1:def 16;

    end;

    theorem :: NCFCONT2:41

    for X be ComplexBanachSpace holds for f be Function of X, X st ex n0 be Element of 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 ComplexBanachSpace;

      let f be Function of X, X;

      given n0 be Element of 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, Th40;

       A4:

      now

        let x be Point of X such that

         A5: (f . x) = x;

        for n be Element of 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];

            

             A8: ( iter (f,n)) is Function of X, X by FUNCT_7: 83;

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

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

            hence P[(n + 1)];

          end;

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

          .= x;

          then

           A9: P[ 0 ];

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

          hence thesis;

        end;

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

        hence xp = x by A3;

      end;

      

       A10: ( iter (f,n0)) is Function of X, X by FUNCT_7: 83;

      (( 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, A10, FUNCT_2: 15;

      then (f . xp) = xp by A3;

      hence thesis by A4;

    end;