ndiff_1.miz



    begin

    reserve n,k for Element of NAT ;

    reserve x,y,X for set;

    reserve g,r,p for Real;

    reserve S for RealNormSpace;

    reserve rseq for Real_Sequence;

    reserve seq,seq1 for sequence of S;

    reserve x0 for Point of S;

    reserve Y for Subset of S;

    theorem :: NDIFF_1:1

    

     Th1: for x0 be Point of S holds for N1,N2 be Neighbourhood of x0 holds ex N be Neighbourhood of x0 st N c= N1 & N c= N2

    proof

      let x0 be Point of S;

      let N1,N2 be Neighbourhood of x0;

      consider g1 be Real such that

       A1: 0 < g1 and

       A2: { y where y be Point of S : ||.(y - x0).|| < g1 } c= N1 by NFCONT_1:def 1;

      consider g2 be Real such that

       A3: 0 < g2 and

       A4: { y where y be Point of S : ||.(y - x0).|| < g2 } c= N2 by NFCONT_1:def 1;

      set g = ( min (g1,g2));

      take { y where y be Point of S : ||.(y - x0).|| < g };

      

       A5: g <= g2 by XXREAL_0: 17;

      

       A6: { y where y be Point of S : ||.(y - x0).|| < g } c= { y where y be Point of S : ||.(y - x0).|| < g2 }

      proof

        let z be object;

        assume z in { y where y be Point of S : ||.(y - x0).|| < g };

        then

        consider y be Point of S such that

         A7: z = y and

         A8: ||.(y - x0).|| < g;

         ||.(y - x0).|| < g2 by A5, A8, XXREAL_0: 2;

        hence thesis by A7;

      end;

      

       A9: g <= g1 by XXREAL_0: 17;

      

       A10: { y where y be Point of S : ||.(y - x0).|| < g } c= { y where y be Point of S : ||.(y - x0).|| < g1 }

      proof

        let z be object;

        assume z in { y where y be Point of S : ||.(y - x0).|| < g };

        then

        consider y be Point of S such that

         A11: z = y and

         A12: ||.(y - x0).|| < g;

         ||.(y - x0).|| < g1 by A9, A12, XXREAL_0: 2;

        hence thesis by A11;

      end;

       0 < g by A1, A3, XXREAL_0: 15;

      hence thesis by A2, A4, A10, A6, NFCONT_1: 3;

    end;

    theorem :: NDIFF_1:2

    

     Th2: for X be Subset of S st X is open holds for r be Point of S st r in X holds ex N be Neighbourhood of r st N c= X

    proof

      let X be Subset of S;

      assume X is open;

      then

       A1: (X ` ) is closed;

      let r be Point of S;

      assume that

       A2: r in X and

       A3: for N be Neighbourhood of r holds not N c= X;

      defpred P[ Element of NAT , Point of S] means $2 in { y where y be Point of S : ||.(y - r).|| < (1 / ($1 + 1)) } & $2 in (X ` );

       A4:

      now

        let g be Real such that

         A5: 0 < g;

        set N = { y where y be Point of S : ||.(y - r).|| < g };

        N is Neighbourhood of r by A5, NFCONT_1: 3;

        then not N c= X by A3;

        then

        consider x be object such that

         A6: x in N and

         A7: not x in X;

        consider s be Point of S such that

         A8: x = s and

         A9: ||.(s - r).|| < g by A6;

        take s;

        thus s in N by A9;

        thus s in (X ` ) by A7, A8, XBOOLE_0:def 5;

      end;

      

       A10: for n holds ex s be Point of S st P[n, s]

      proof

        let n;

         0 < (1 * ((n + 1) " ));

        then 0 < (1 / (n + 1)) by XCMPLX_0:def 9;

        hence thesis by A4;

      end;

      consider s1 be sequence of S such that

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

      

       A12: ( rng s1) c= (X ` )

      proof

        let x be object;

        assume x in ( rng s1);

        then

        consider y be object such that

         A13: y in ( dom s1) and

         A14: (s1 . y) = x by FUNCT_1:def 3;

        reconsider y as Element of NAT by A13;

        (s1 . y) in (X ` ) by A11;

        hence thesis by A14;

      end;

       A15:

      now

        let p be Real;

        assume

         A16: 0 < p;

        consider n be Nat such that

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

        ((p " ) + 0 ) < (n + 1) by A17, XREAL_1: 8;

        then (1 / (n + 1)) < (1 / (p " )) by A16, XREAL_1: 76;

        then

         A18: (1 / (n + 1)) < p by XCMPLX_1: 216;

        take n;

        let m be Nat;

        

         A19: m in NAT by ORDINAL1:def 12;

        assume n <= m;

        then

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

        (s1 . m) in { y where y be Point of S : ||.(y - r).|| < (1 / (m + 1)) } by A11, A19;

        then

         A21: ex y be Point of S st (s1 . m) = y & ||.(y - r).|| < (1 / (m + 1));

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

        then ||.((s1 . m) - r).|| < (1 / (n + 1)) by A21, XXREAL_0: 2;

        hence ||.((s1 . m) - r).|| < p by A18, XXREAL_0: 2;

      end;

      then

       A22: s1 is convergent;

      then ( lim s1) = r by A15, NORMSP_1:def 7;

      then r in (X ` ) by A22, A12, A1;

      hence contradiction by A2, XBOOLE_0:def 5;

    end;

    theorem :: NDIFF_1:3

    for X be Subset of S st X is open holds for r be Point of S st r in X holds ex g st 0 < g & { y where y be Point of S : ||.(y - r).|| < g } c= X

    proof

      let X be Subset of S such that

       A1: X is open;

      let r be Point of S;

      assume r in X;

      then

      consider N be Neighbourhood of r such that

       A2: N c= X by A1, Th2;

      consider g such that

       A3: 0 < g & { y where y be Point of S : ||.(y - r).|| < g } c= N by NFCONT_1:def 1;

      take g;

      thus thesis by A2, A3;

    end;

    theorem :: NDIFF_1:4

    

     Th4: for X be Subset of S holds ((for r be Point of S st r in X holds ex N be Neighbourhood of r st N c= X) implies X is open)

    proof

      let X be Subset of S;

      assume that

       A1: for r be Point of S st r in X holds ex N be Neighbourhood of r st N c= X and

       A2: not X is open;

       not (X ` ) is closed by A2;

      then

      consider s1 be sequence of S such that

       A3: ( rng s1) c= (X ` ) and

       A4: s1 is convergent and

       A5: not ( lim s1) in (X ` );

      consider N be Neighbourhood of ( lim s1) such that

       A6: N c= X by A1, A5, SUBSET_1: 29;

      consider g be Real such that

       A7: 0 < g and

       A8: { y where y be Point of S : ||.(y - ( lim s1)).|| < g } c= N by NFCONT_1:def 1;

      consider n be Nat such that

       A9: for m be Nat st n <= m holds ||.((s1 . m) - ( lim s1)).|| < g by A4, A7, NORMSP_1:def 7;

      n in NAT by ORDINAL1:def 12;

      then n in ( dom s1) by FUNCT_2:def 1;

      then

       A10: (s1 . n) in ( rng s1) by FUNCT_1:def 3;

       ||.((s1 . n) - ( lim s1)).|| < g by A9;

      then (s1 . n) in { y where y be Point of S : ||.(y - ( lim s1)).|| < g };

      then (s1 . n) in N by A8;

      hence contradiction by A3, A6, A10, XBOOLE_0:def 5;

    end;

    theorem :: NDIFF_1:5

    for X be Subset of S holds ((for r be Point of S st r in X holds ex N be Neighbourhood of r st N c= X) iff X is open) by Th2, Th4;

    definition

      let X be set, S be ZeroStr;

      let f be Function of X, S;

      :: original: non-zero

      redefine

      :: NDIFF_1:def1

      attr f is non-zero means ( rng f) c= ( NonZero S);

      compatibility

      proof

        thus f is non-zero implies ( rng f) c= ( NonZero S) by ZFMISC_1: 34;

        assume

         A1: ( rng f) c= ( NonZero S);

        assume ( 0. S) in ( rng f);

        then not ( 0. S) in {( 0. S)} by A1, XBOOLE_0:def 5;

        hence contradiction by TARSKI:def 1;

      end;

    end

    theorem :: NDIFF_1:6

    

     Th6: seq is non-zero iff for x st x in NAT holds (seq . x) <> ( 0. S)

    proof

      thus seq is non-zero implies for x st x in NAT holds (seq . x) <> ( 0. S)

      proof

        assume seq is non-zero;

        then

         A1: ( rng seq) c= ( NonZero S);

        let x;

        assume x in NAT ;

        then x in ( dom seq) by FUNCT_2:def 1;

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

        then not (seq . x) in {( 0. S)} by A1, XBOOLE_0:def 5;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A2: for x st x in NAT holds (seq . x) <> ( 0. S);

      now

        let y be object;

        assume

         A3: y in ( rng seq);

        then ex x be object st x in ( dom seq) & (seq . x) = y by FUNCT_1:def 3;

        then y <> ( 0. S) by A2;

        then not y in {( 0. S)} by TARSKI:def 1;

        hence y in ( NonZero S) by A3, XBOOLE_0:def 5;

      end;

      then ( rng seq) c= ( NonZero S);

      hence thesis;

    end;

    theorem :: NDIFF_1:7

    

     Th7: seq is non-zero iff for n be Nat holds (seq . n) <> ( 0. S)

    proof

      thus seq is non-zero implies for n be Nat holds (seq . n) <> ( 0. S) by ORDINAL1:def 12, Th6;

      assume for n be Nat holds (seq . n) <> ( 0. S);

      then for x holds x in NAT implies (seq . x) <> ( 0. S);

      hence thesis by Th6;

    end;

    definition

      let RNS be RealLinearSpace;

      let S be sequence of RNS;

      let a be Real_Sequence;

      :: NDIFF_1:def2

      func a (#) S -> sequence of RNS means

      : Def2: for n be Nat holds (it . n) = ((a . n) * (S . n));

      existence

      proof

        deffunc F( Element of NAT ) = ((a . $1) * (S . $1));

        consider S be sequence of RNS such that

         A1: for n holds (S . n) = F(n) from FUNCT_2:sch 4;

        take S;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of RNS;

        assume that

         A2: for n be Nat holds (S1 . n) = ((a . n) * (S . n)) and

         A3: for n be Nat holds (S2 . n) = ((a . n) * (S . n));

        for n holds (S1 . n) = (S2 . n)

        proof

          let n;

          (S1 . n) = ((a . n) * (S . n)) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let RNS be RealLinearSpace;

      let z be Point of RNS;

      let a be Real_Sequence;

      :: NDIFF_1:def3

      func a * z -> sequence of RNS means

      : Def3: for n be Nat holds (it . n) = ((a . n) * z);

      existence

      proof

        deffunc F( Element of NAT ) = ((a . $1) * z);

        consider S be sequence of RNS such that

         A1: for n holds (S . n) = F(n) from FUNCT_2:sch 4;

        take S;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of RNS;

        assume that

         A2: for n be Nat holds (S1 . n) = ((a . n) * z) and

         A3: for n be Nat holds (S2 . n) = ((a . n) * z);

        for n holds (S1 . n) = (S2 . n)

        proof

          let n;

          (S1 . n) = ((a . n) * z) by A2;

          hence thesis by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: NDIFF_1:8

    for rseq1,rseq2 be Real_Sequence holds ((rseq1 + rseq2) (#) seq) = ((rseq1 (#) seq) + (rseq2 (#) seq))

    proof

      let rseq1,rseq2 be Real_Sequence;

      now

        let n;

        

        thus (((rseq1 + rseq2) (#) seq) . n) = (((rseq1 + rseq2) . n) * (seq . n)) by Def2

        .= (((rseq1 . n) + (rseq2 . n)) * (seq . n)) by SEQ_1: 7

        .= (((rseq1 . n) * (seq . n)) + ((rseq2 . n) * (seq . n))) by RLVECT_1:def 6

        .= (((rseq1 (#) seq) . n) + ((rseq2 . n) * (seq . n))) by Def2

        .= (((rseq1 (#) seq) . n) + ((rseq2 (#) seq) . n)) by Def2

        .= (((rseq1 (#) seq) + (rseq2 (#) seq)) . n) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_1:9

    

     Th9: for rseq be Real_Sequence holds for seq1,seq2 be sequence of S holds (rseq (#) (seq1 + seq2)) = ((rseq (#) seq1) + (rseq (#) seq2))

    proof

      let rseq be Real_Sequence;

      let seq1,seq2 be sequence of S;

      now

        let n;

        

        thus ((rseq (#) (seq1 + seq2)) . n) = ((rseq . n) * ((seq1 + seq2) . n)) by Def2

        .= ((rseq . n) * ((seq1 . n) + (seq2 . n))) by NORMSP_1:def 2

        .= (((rseq . n) * (seq1 . n)) + ((rseq . n) * (seq2 . n))) by RLVECT_1:def 5

        .= (((rseq (#) seq1) . n) + ((rseq . n) * (seq2 . n))) by Def2

        .= (((rseq (#) seq1) . n) + ((rseq (#) seq2) . n)) by Def2

        .= (((rseq (#) seq1) + (rseq (#) seq2)) . n) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_1:10

    

     Th10: for rseq be Real_Sequence holds (r * (rseq (#) seq)) = (rseq (#) (r * seq))

    proof

      let rseq be Real_Sequence;

      now

        let n;

        

        thus ((r * (rseq (#) seq)) . n) = (r * ((rseq (#) seq) . n)) by NORMSP_1:def 5

        .= (r * ((rseq . n) * (seq . n))) by Def2

        .= ((r * (rseq . n)) * (seq . n)) by RLVECT_1:def 7

        .= ((rseq . n) * (r * (seq . n))) by RLVECT_1:def 7

        .= ((rseq . n) * ((r * seq) . n)) by NORMSP_1:def 5

        .= ((rseq (#) (r * seq)) . n) by Def2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_1:11

    for rseq1,rseq2 be Real_Sequence holds ((rseq1 - rseq2) (#) seq) = ((rseq1 (#) seq) - (rseq2 (#) seq))

    proof

      let rseq1,rseq2 be Real_Sequence;

      now

        let n;

        

        thus (((rseq1 - rseq2) (#) seq) . n) = (((rseq1 + ( - rseq2)) . n) * (seq . n)) by Def2

        .= (((rseq1 . n) + (( - rseq2) . n)) * (seq . n)) by SEQ_1: 7

        .= (((rseq1 . n) + ( - (rseq2 . n))) * (seq . n)) by SEQ_1: 10

        .= (((rseq1 . n) - (rseq2 . n)) * (seq . n))

        .= (((rseq1 . n) * (seq . n)) - ((rseq2 . n) * (seq . n))) by RLVECT_1: 35

        .= (((rseq1 (#) seq) . n) - ((rseq2 . n) * (seq . n))) by Def2

        .= (((rseq1 (#) seq) . n) - ((rseq2 (#) seq) . n)) by Def2

        .= (((rseq1 (#) seq) - (rseq2 (#) seq)) . n) by NORMSP_1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_1:12

    

     Th12: for rseq be Real_Sequence holds for seq1,seq2 be sequence of S holds (rseq (#) (seq1 - seq2)) = ((rseq (#) seq1) - (rseq (#) seq2))

    proof

      let rseq be Real_Sequence;

      let seq1,seq2 be sequence of S;

      now

        let n;

        

        thus ((rseq (#) (seq1 - seq2)) . n) = ((rseq . n) * ((seq1 - seq2) . n)) by Def2

        .= ((rseq . n) * ((seq1 . n) - (seq2 . n))) by NORMSP_1:def 3

        .= (((rseq . n) * (seq1 . n)) - ((rseq . n) * (seq2 . n))) by RLVECT_1: 34

        .= (((rseq (#) seq1) . n) - ((rseq . n) * (seq2 . n))) by Def2

        .= (((rseq (#) seq1) . n) - ((rseq (#) seq2) . n)) by Def2

        .= (((rseq (#) seq1) - (rseq (#) seq2)) . n) by NORMSP_1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_1:13

    

     Th13: rseq is convergent & seq is convergent implies (rseq (#) seq) is convergent

    proof

      assume that

       A1: rseq is convergent and

       A2: seq is convergent;

      consider g1 be Real such that

       A3: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((rseq . m) - g1).| < p by A1, SEQ_2:def 6;

      consider g2 be Point of S such that

       A4: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - g2).|| < p by A2;

      reconsider g1 as Real;

      take g = (g1 * g2);

      let p;

      rseq is bounded by A1, SEQ_2: 13;

      then

      consider r be Real such that

       A5: 0 < r and

       A6: for n be Nat holds |.(rseq . n).| < r by SEQ_2: 3;

      reconsider r as Real;

      

       A7: ( 0 + 0 ) < ( ||.g2.|| + r) by A5, NORMSP_1: 4, XREAL_1: 8;

      assume

       A8: 0 < p;

      then

      consider n1 be Nat such that

       A9: for m be Nat st n1 <= m holds |.((rseq . m) - g1).| < (p / ( ||.g2.|| + r)) by A3, A7, XREAL_1: 139;

      consider n2 be Nat such that

       A10: for m be Nat st n2 <= m holds ||.((seq . m) - g2).|| < (p / ( ||.g2.|| + r)) by A4, A7, A8, XREAL_1: 139;

      reconsider n = (n1 + n2) as Nat;

      take n;

      let m be Nat such that

       A11: n <= m;

      n1 <= (n1 + n2) by NAT_1: 12;

      then n1 <= m by A11, XXREAL_0: 2;

      then

       A12: |.((rseq . m) - g1).| <= (p / ( ||.g2.|| + r)) by A9;

       0 <= ||.g2.|| & ||.(((rseq . m) - g1) * g2).|| = ( ||.g2.|| * |.((rseq . m) - g1).|) by NORMSP_1: 4, NORMSP_1:def 1;

      then

       A13: ||.(((rseq . m) - g1) * g2).|| <= ( ||.g2.|| * (p / ( ||.g2.|| + r))) by A12, XREAL_1: 64;

       ||.(((rseq (#) seq) . m) - g).|| = ||.(((rseq . m) * (seq . m)) - (g1 * g2)).|| by Def2

      .= ||.((((rseq . m) * (seq . m)) - ( 0. S)) - (g1 * g2)).|| by RLVECT_1: 13

      .= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * g2) - ((rseq . m) * g2))) - (g1 * g2)).|| by RLVECT_1: 15

      .= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1: 29

      .= ||.((((rseq . m) * ((seq . m) - g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1: 34

      .= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) * g2) - (g1 * g2))).|| by RLVECT_1:def 3

      .= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) - g1) * g2)).|| by RLVECT_1: 35;

      then

       A14: ||.(((rseq (#) seq) . m) - g).|| <= ( ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).||) by NORMSP_1:def 1;

      n2 <= n by NAT_1: 12;

      then n2 <= m by A11, XXREAL_0: 2;

      then

       A15: ||.((seq . m) - g2).|| < (p / ( ||.g2.|| + r)) by A10;

      

       A16: 0 <= |.(rseq . m).| & 0 <= ||.((seq . m) - g2).|| by COMPLEX1: 46, NORMSP_1: 4;

       |.(rseq . m).| < r by A6;

      then ( |.(rseq . m).| * ||.((seq . m) - g2).||) < (r * (p / ( ||.g2.|| + r))) by A16, A15, XREAL_1: 96;

      then

       A17: ||.((rseq . m) * ((seq . m) - g2)).|| < (r * (p / ( ||.g2.|| + r))) by NORMSP_1:def 1;

      ((r * (p / ( ||.g2.|| + r))) + ( ||.g2.|| * (p / ( ||.g2.|| + r)))) = ((p / ( ||.g2.|| + r)) * ( ||.g2.|| + r))

      .= p by A7, XCMPLX_1: 87;

      then ( ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).||) < p by A17, A13, XREAL_1: 8;

      hence thesis by A14, XXREAL_0: 2;

    end;

    theorem :: NDIFF_1:14

    

     Th14: rseq is convergent & seq is convergent implies ( lim (rseq (#) seq)) = (( lim rseq) * ( lim seq))

    proof

      assume that

       A1: rseq is convergent and

       A2: seq is convergent;

      set g2 = ( lim seq);

      reconsider g1 = ( lim rseq) as Real;

      set g = (g1 * g2);

      rseq is bounded by A1, SEQ_2: 13;

      then

      consider r be Real such that

       A3: 0 < r and

       A4: for n be Nat holds |.(rseq . n).| < r by SEQ_2: 3;

      reconsider r as Real;

      

       A5: ( 0 + 0 ) < ( ||.g2.|| + r) by A3, NORMSP_1: 4, XREAL_1: 8;

      

       A6: 0 <= ||.g2.|| by NORMSP_1: 4;

      

       A7: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ||.(((rseq (#) seq) . m) - g).|| < p

      proof

        let p be Real;

        assume 0 < p;

        then

         A8: 0 < (p / ( ||.g2.|| + r)) by A5, XREAL_1: 139;

        then

        consider n1 be Nat such that

         A9: for m be Nat st n1 <= m holds |.((rseq . m) - g1).| < (p / ( ||.g2.|| + r)) by A1, SEQ_2:def 7;

        consider n2 be Nat such that

         A10: for m be Nat st n2 <= m holds ||.((seq . m) - g2).|| < (p / ( ||.g2.|| + r)) by A2, A8, NORMSP_1:def 7;

        take n = (n1 + n2);

        let m be Nat such that

         A11: n <= m;

        n1 <= (n1 + n2) by NAT_1: 12;

        then n1 <= m by A11, XXREAL_0: 2;

        then

         A12: |.((rseq . m) - g1).| <= (p / ( ||.g2.|| + r)) by A9;

         ||.(((rseq . m) - g1) * g2).|| = ( ||.g2.|| * |.((rseq . m) - g1).|) by NORMSP_1:def 1;

        then

         A13: ||.(((rseq . m) - g1) * g2).|| <= ( ||.g2.|| * (p / ( ||.g2.|| + r))) by A6, A12, XREAL_1: 64;

        

         A14: 0 <= |.(rseq . m).| & 0 <= ||.((seq . m) - g2).|| by COMPLEX1: 46, NORMSP_1: 4;

        n2 <= n by NAT_1: 12;

        then n2 <= m by A11, XXREAL_0: 2;

        then

         A15: ||.((seq . m) - g2).|| < (p / ( ||.g2.|| + r)) by A10;

         ||.(((rseq (#) seq) . m) - g).|| = ||.(((rseq . m) * (seq . m)) - (g1 * g2)).|| by Def2

        .= ||.((((rseq . m) * (seq . m)) - ( 0. S)) - (g1 * g2)).|| by RLVECT_1: 13

        .= ||.((((rseq . m) * (seq . m)) - (((rseq . m) * g2) - ((rseq . m) * g2))) - (g1 * g2)).|| by RLVECT_1: 15

        .= ||.(((((rseq . m) * (seq . m)) - ((rseq . m) * g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1: 29

        .= ||.((((rseq . m) * ((seq . m) - g2)) + ((rseq . m) * g2)) - (g1 * g2)).|| by RLVECT_1: 34

        .= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) * g2) - (g1 * g2))).|| by RLVECT_1:def 3

        .= ||.(((rseq . m) * ((seq . m) - g2)) + (((rseq . m) - g1) * g2)).|| by RLVECT_1: 35;

        then

         A16: ||.(((rseq (#) seq) . m) - g).|| <= ( ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).||) by NORMSP_1:def 1;

         |.(rseq . m).| < r by A4;

        then ( |.(rseq . m).| * ||.((seq . m) - g2).||) < (r * (p / ( ||.g2.|| + r))) by A14, A15, XREAL_1: 96;

        then

         A17: ||.((rseq . m) * ((seq . m) - g2)).|| < (r * (p / ( ||.g2.|| + r))) by NORMSP_1:def 1;

        ((r * (p / ( ||.g2.|| + r))) + ( ||.g2.|| * (p / ( ||.g2.|| + r)))) = ((p / ( ||.g2.|| + r)) * ( ||.g2.|| + r))

        .= p by A5, XCMPLX_1: 87;

        then ( ||.((rseq . m) * ((seq . m) - g2)).|| + ||.(((rseq . m) - g1) * g2).||) < p by A17, A13, XREAL_1: 8;

        hence thesis by A16, XXREAL_0: 2;

      end;

      (rseq (#) seq) is convergent by A1, A2, Th13;

      hence thesis by A7, NORMSP_1:def 7;

    end;

    theorem :: NDIFF_1:15

    

     Th15: for k be Nat holds ((seq + seq1) ^\ k) = ((seq ^\ k) + (seq1 ^\ k))

    proof

      let k be Nat;

      now

        let n;

        

        thus (((seq + seq1) ^\ k) . n) = ((seq + seq1) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) + (seq1 . (n + k))) by NORMSP_1:def 2

        .= (((seq ^\ k) . n) + (seq1 . (n + k))) by NAT_1:def 3

        .= (((seq ^\ k) . n) + ((seq1 ^\ k) . n)) by NAT_1:def 3

        .= (((seq ^\ k) + (seq1 ^\ k)) . n) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_1:16

    

     Th16: ((seq - seq1) ^\ k) = ((seq ^\ k) - (seq1 ^\ k))

    proof

      now

        let n;

        

        thus (((seq - seq1) ^\ k) . n) = ((seq - seq1) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) - (seq1 . (n + k))) by NORMSP_1:def 3

        .= (((seq ^\ k) . n) - (seq1 . (n + k))) by NAT_1:def 3

        .= (((seq ^\ k) . n) - ((seq1 ^\ k) . n)) by NAT_1:def 3

        .= (((seq ^\ k) - (seq1 ^\ k)) . n) by NORMSP_1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NDIFF_1:17

    

     Th17: seq is non-zero implies (seq ^\ k) is non-zero

    proof

      assume

       A1: seq is non-zero;

      now

        let n be Nat;

        ((seq ^\ k) . n) = (seq . (n + k)) by NAT_1:def 3;

        hence ((seq ^\ k) . n) <> ( 0. S) by A1, Th7;

      end;

      hence thesis by Th7;

    end;

    definition

      let S;

      let x be Point of S;

      let IT be sequence of S;

      :: NDIFF_1:def4

      attr IT is x -convergent means

      : Def4: IT is convergent & ( lim IT) = x;

    end

    theorem :: NDIFF_1:18

    

     Th18: for X be RealNormSpace holds for seq be sequence of X holds seq is constant implies (seq is convergent & for k be Element of NAT holds ( lim seq) = (seq . k))

    proof

      let X be RealNormSpace;

      let seq be sequence of X;

      assume

       A1: seq is constant;

      then

      consider r be Point of X such that

       A2: for n be Nat holds (seq . n) = r by VALUED_0:def 18;

      thus

       A3: seq is convergent by A1, LOPBAN_3: 12;

      now

        let k be Element of NAT ;

        now

          let p be Real such that

           A4: 0 < p;

          reconsider n = 0 as Nat;

          take n;

          let m be Nat such that n <= m;

           ||.((seq . m) - (seq . k)).|| = ||.(r - (seq . k)).|| by A2

          .= ||.(r - r).|| by A2

          .= ||.( 0. X).|| by RLVECT_1: 15

          .= 0 by NORMSP_1: 1;

          hence ||.((seq . m) - (seq . k)).|| < p by A4;

        end;

        hence ( lim seq) = (seq . k) by A3, NORMSP_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_1:19

    

     Th19: for r be Real st 0 < r & (for n be Nat holds (seq . n) = ((1 / (n + r)) * x0)) holds seq is convergent

    proof

      let r be Real;

      assume that

       A1: 0 < r and

       A2: for n be Nat holds (seq . n) = ((1 / (n + r)) * x0);

      take g = ( 0. S);

      let p be Real;

      assume

       A3: 0 < p;

      ex pp be Real st pp > 0 & (pp * ||.x0.||) < p

      proof

        take pp = (p / ( ||.x0.|| + 1));

        

         A4: ( ||.x0.|| + 0 ) < ( ||.x0.|| + 1) & 0 <= ||.x0.|| by NORMSP_1: 4, XREAL_1: 8;

        

         A5: ( ||.x0.|| + 1) > ( 0 + 0 ) by NORMSP_1: 4, XREAL_1: 8;

        then 0 < (p / ( ||.x0.|| + 1)) by A3, XREAL_1: 139;

        then (pp * ||.x0.||) < (pp * ( ||.x0.|| + 1)) by A4, XREAL_1: 97;

        hence thesis by A3, A5, XCMPLX_1: 87;

      end;

      then

      consider pp be Real such that

       A6: pp > 0 and

       A7: (pp * ||.x0.||) < p;

      consider k1 be Nat such that

       A8: (pp " ) < k1 by SEQ_4: 3;

      ((pp " ) + 0 ) < (k1 + r) by A1, A8, XREAL_1: 8;

      then (1 / (k1 + r)) < (1 / (pp " )) by A6, XREAL_1: 76;

      then

       A9: (1 / (k1 + r)) < (1 * ((pp " ) " )) by XCMPLX_0:def 9;

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

      take n = k1;

      let m be Nat;

      assume n <= m;

      then

       A10: (n + r) <= (m + r) by XREAL_1: 6;

      

       A11: 0 <= ||.x0.|| by NORMSP_1: 4;

      (1 / (m + r)) <= (1 / (n + r)) by A1, A10, XREAL_1: 118;

      then (1 / (m + r)) < pp by A9, XXREAL_0: 2;

      then

       A12: ((1 / (m + r)) * ||.x0.||) <= (pp * ||.x0.||) by A11, XREAL_1: 64;

       ||.((seq . m) - g).|| = ||.(((1 / (m + r)) * x0) - ( 0. S)).|| by A2

      .= ||.((1 / (m + r)) * x0).|| by RLVECT_1: 13

      .= ( |.(1 / (m + r)).| * ||.x0.||) by NORMSP_1:def 1

      .= ((1 / (m + r)) * ||.x0.||) by A1, ABSVALUE:def 1;

      hence thesis by A7, A12, XXREAL_0: 2;

    end;

    theorem :: NDIFF_1:20

    

     Th20: for r be Real st 0 < r & (for n be Nat holds (seq . n) = ((1 / (n + r)) * x0)) holds ( lim seq) = ( 0. S)

    proof

      let r be Real;

      assume that

       A1: 0 < r and

       A2: for n be Nat holds (seq . n) = ((1 / (n + r)) * x0);

       A3:

      now

        let p;

        

         A4: 0 <= ||.x0.|| by NORMSP_1: 4;

        assume

         A5: 0 < p;

        ex pp be Real st pp > 0 & (pp * ||.x0.||) < p

        proof

          take pp = (p / ( ||.x0.|| + 1));

          

           A6: ( ||.x0.|| + 0 ) < ( ||.x0.|| + 1) & 0 <= ||.x0.|| by NORMSP_1: 4, XREAL_1: 8;

          

           A7: ( ||.x0.|| + 1) > ( 0 + 0 ) by NORMSP_1: 4, XREAL_1: 8;

          then 0 < (p / ( ||.x0.|| + 1)) by A5, XREAL_1: 139;

          then (pp * ||.x0.||) < (pp * ( ||.x0.|| + 1)) by A6, XREAL_1: 97;

          hence thesis by A5, A7, XCMPLX_1: 87;

        end;

        then

        consider pp be Real such that

         A8: pp > 0 and

         A9: (pp * ||.x0.||) < p;

        consider k1 be Nat such that

         A10: (pp " ) < k1 by SEQ_4: 3;

        ((pp " ) + 0 ) < (k1 + r) by A1, A10, XREAL_1: 8;

        then (1 / (k1 + r)) < (1 / (pp " )) by A8, XREAL_1: 76;

        then

         A11: (1 / (k1 + r)) < (1 * ((pp " ) " )) by XCMPLX_0:def 9;

        reconsider n = k1 as Nat;

        take n;

        let m be Nat;

        assume n <= m;

        then

         A12: (n + r) <= (m + r) by XREAL_1: 6;

        (1 / (m + r)) <= (1 / (n + r)) by A1, A12, XREAL_1: 118;

        then (1 / (m + r)) < pp by A11, XXREAL_0: 2;

        then

         A13: ((1 / (m + r)) * ||.x0.||) <= (pp * ||.x0.||) by A4, XREAL_1: 64;

         ||.((seq . m) - ( 0. S)).|| = ||.(((1 / (m + r)) * x0) - ( 0. S)).|| by A2

        .= ||.((1 / (m + r)) * x0).|| by RLVECT_1: 13

        .= ( |.(1 / (m + r)).| * ||.x0.||) by NORMSP_1:def 1

        .= ((1 / (m + r)) * ||.x0.||) by A1, ABSVALUE:def 1;

        hence ||.((seq . m) - ( 0. S)).|| < p by A9, A13, XXREAL_0: 2;

      end;

      seq is convergent by A1, A2, Th19;

      hence thesis by A3, NORMSP_1:def 7;

    end;

    registration

      let S be non trivial RealNormSpace;

      cluster non-zero( 0. S) -convergent for sequence of S;

      existence

      proof

        consider x0 be Point of S such that

         A1: x0 <> ( 0. S) by STRUCT_0:def 18;

        deffunc F( Nat) = ((1 / ($1 + 1)) * x0);

        consider s1 be sequence of S such that

         A2: for n holds (s1 . n) = F(n) from FUNCT_2:sch 4;

        

         A3: for n be Nat holds (s1 . n) = F(n)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A2;

        end;

        take s1;

        now

          let n be Nat;

          ((n + 1) " ) <> 0 ;

          then

           A4: (1 / (n + 1)) <> 0 by XCMPLX_1: 215;

          thus (s1 . n) <> ( 0. S)

          proof

            assume (s1 . n) = ( 0. S);

            then ((1 / (n + 1)) * x0) = ( 0. S) by A3;

            hence contradiction by A1, A4, RLVECT_1: 11;

          end;

        end;

        hence s1 is non-zero by Th7;

        

         A5: ( lim s1) = ( 0. S) by A3, Th20;

        s1 is convergent by A3, Th19;

        then s1 is ( 0. S) -convergent by A5;

        hence thesis;

      end;

    end

    registration

      let S be RealNormSpace;

      cluster ( 0. S) -convergent for sequence of S;

      existence

      proof

        set x0 = the Point of S;

        deffunc F( Nat) = ((1 / ($1 + 1)) * x0);

        consider s1 be sequence of S such that

         A1: for n holds (s1 . n) = F(n) from FUNCT_2:sch 4;

        

         A2: for n be Nat holds (s1 . n) = F(n)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A1;

        end;

        take s1;

        

         A3: ( lim s1) = ( 0. S) by A2, Th20;

        s1 is convergent by A2, Th19;

        then s1 is ( 0. S) -convergent by A3;

        hence thesis;

      end;

    end

    theorem :: NDIFF_1:21

    for a be 0 -convergent non-zero Real_Sequence holds for z be Point of S st z <> ( 0. S) holds (a * z) is non-zero( 0. S) -convergent

    proof

      let a be 0 -convergent non-zero Real_Sequence;

      let z be Point of S such that

       A1: z <> ( 0. S);

      now

        let n be Nat;

        

         A2: (a . n) <> 0 by SEQ_1: 5;

        assume ((a * z) . n) = ( 0. S);

        then ((a . n) * z) = ( 0. S) by Def3;

        hence contradiction by A1, A2, RLVECT_1: 11;

      end;

      hence (a * z) is non-zero by Th7;

       A3:

      now

        let p;

        assume

         A4: 0 < p;

        ex pp be Real st pp > 0 & (pp * ||.z.||) < p

        proof

          take pp = (p / ( ||.z.|| + 1));

          

           A5: ( ||.z.|| + 0 ) < ( ||.z.|| + 1) & 0 <= ||.z.|| by NORMSP_1: 4, XREAL_1: 8;

          

           A6: ( ||.z.|| + 1) > ( 0 + 0 ) by NORMSP_1: 4, XREAL_1: 8;

          then 0 < (p / ( ||.z.|| + 1)) by A4, XREAL_1: 139;

          then (pp * ||.z.||) < (pp * ( ||.z.|| + 1)) by A5, XREAL_1: 97;

          hence thesis by A4, A6, XCMPLX_1: 87;

        end;

        then

        consider pp be Real such that

         A7: pp > 0 and

         A8: (pp * ||.z.||) < p;

        a is convergent & ( lim a) = 0 ;

        then

        consider n be Nat such that

         A9: for m be Nat st n <= m holds |.((a . m) - 0 ).| < pp by A7, SEQ_2:def 7;

        reconsider n as Nat;

        take n;

        let m be Nat;

        assume n <= m;

        then

         A10: |.((a . m) - 0 ).| < pp by A9;

        

         A11: ||.(((a * z) . m) - ( 0. S)).|| = ||.(((a . m) * z) - ( 0. S)).|| by Def3

        .= ||.((a . m) * z).|| by RLVECT_1: 13

        .= ( |.(a . m).| * ||.z.||) by NORMSP_1:def 1;

         0 <= ||.z.|| by NORMSP_1: 4;

        then ( |.(a . m).| * ||.z.||) <= (pp * ||.z.||) by A10, XREAL_1: 64;

        hence ||.(((a * z) . m) - ( 0. S)).|| < p by A8, A11, XXREAL_0: 2;

      end;

      hence (a * z) is convergent;

      hence thesis by A3, NORMSP_1:def 7;

    end;

    theorem :: NDIFF_1:22

    (for r be Point of S holds r in Y iff r in the carrier of S) iff Y = the carrier of S

    proof

      thus (for r be Point of S holds r in Y iff r in the carrier of S) implies Y = the carrier of S

      proof

        assume for r be Point of S holds r in Y iff r in the carrier of S;

        then for y be object holds y in Y iff y in the carrier of S;

        hence thesis by TARSKI: 2;

      end;

      assume

       A1: Y = the carrier of S;

      let r be Point of S;

      thus r in Y implies r in the carrier of S;

      thus thesis by A1;

    end;

    reserve S,T for RealNormSpace;

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

    reserve s1 for sequence of S;

    reserve x0 for Point of S;

    registration

      let S;

      cluster constant for sequence of S;

      existence

      proof

        reconsider s1 = ( NAT --> ( 0. S)) as sequence of S;

        take s1;

        thus thesis;

      end;

    end

    reserve h for ( 0. S) -convergent sequence of S;

    reserve c for constant sequence of S;

    definition

      let S, T;

      let IT be PartFunc of S, T;

      :: NDIFF_1:def5

      attr IT is RestFunc-like means

      : Def5: IT is total & for h st h is non-zero holds (( ||.h.|| " ) (#) (IT /* h)) is convergent & ( lim (( ||.h.|| " ) (#) (IT /* h))) = ( 0. T);

    end

    registration

      let S, T;

      cluster RestFunc-like for PartFunc of S, T;

      existence

      proof

        reconsider f = (the carrier of S --> ( 0. T)) as PartFunc of S, T;

        take f;

        thus f is total;

        

         A1: ( dom f) = the carrier of S;

        now

          let h;

          assume h is non-zero;

          now

            let n be Nat;

            

             A2: (f /. (h . n)) = (f . (h . n)) by A1, PARTFUN1:def 6

            .= ( 0. T);

            

             A3: ( rng h) c= ( dom f);

            

             A4: n in NAT by ORDINAL1:def 12;

            

            thus ((( ||.h.|| " ) (#) (f /* h)) . n) = ((( ||.h.|| " ) . n) * ((f /* h) . n)) by Def2

            .= ((( ||.h.|| " ) . n) * (f /. (h . n))) by A3, A4, FUNCT_2: 109

            .= ( 0. T) by A2, RLVECT_1: 10;

          end;

          then (( ||.h.|| " ) (#) (f /* h)) is constant & ((( ||.h.|| " ) (#) (f /* h)) . 0 ) = ( 0. T) by VALUED_0:def 18;

          hence (( ||.h.|| " ) (#) (f /* h)) is convergent & ( lim (( ||.h.|| " ) (#) (f /* h))) = ( 0. T) by Th18;

        end;

        hence thesis;

      end;

    end

    definition

      let S, T;

      mode RestFunc of S,T is RestFunc-like PartFunc of S, T;

    end

    theorem :: NDIFF_1:23

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

    proof

      let R be PartFunc of S, T such that

       A1: R is total;

       A2:

      now

        assume

         A3: R is RestFunc-like;

        assume not (for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Point of S st z <> ( 0. S) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r);

        then

        consider r be Real such that

         A4: r > 0 and

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

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

        

         A6: for n be Element of NAT holds ex z be Point of S st P[n, z]

        proof

          let n be Element of NAT ;

           0 < (1 * ((n + 1) " ));

          then 0 < (1 / (n + 1)) by XCMPLX_0:def 9;

          hence thesis by A5;

        end;

        consider s be sequence of S such that

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

        

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

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A7;

        end;

         A9:

        now

          let p be Real;

          assume

           A10: 0 < p;

          consider n be Nat such that

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

          ((p " ) + 0 ) < (n + 1) by A11, XREAL_1: 8;

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

          then

           A12: (1 / (n + 1)) < p by XCMPLX_1: 216;

          reconsider n as Nat;

          take n;

          let m be Nat;

          assume n <= m;

          then

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

           ||.(s . m).|| < (1 / (m + 1)) by A8;

          then

           A14: ||.((s . m) - ( 0. S)).|| < (1 / (m + 1)) by RLVECT_1: 13;

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

          then ||.((s . m) - ( 0. S)).|| < (1 / (n + 1)) by A14, XXREAL_0: 2;

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

        end;

        then

         A15: s is convergent;

        then ( lim s) = ( 0. S) by A9, NORMSP_1:def 7;

        then

        reconsider s as ( 0. S) -convergent sequence of S by A15, Def4;

        s is non-zero by A8, Th7;

        then (( ||.s.|| " ) (#) (R /* s)) is convergent & ( lim (( ||.s.|| " ) (#) (R /* s))) = ( 0. T) by A3;

        then

        consider n be Nat such that

         A16: for m be Nat st n <= m holds ||.(((( ||.s.|| " ) (#) (R /* s)) . m) - ( 0. T)).|| < r by A4, NORMSP_1:def 7;

        

         A17: n in NAT by ORDINAL1:def 12;

        

         A18: ||.(((( ||.s.|| " ) (#) (R /* s)) . n) - ( 0. T)).|| < r by A16;

        (s . n) <> ( 0. S) by A8;

        then ||.(s . n).|| <> 0 by NORMSP_0:def 5;

        then

         A19: ||.(s . n).|| > 0 by NORMSP_1: 4;

        

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

        .= (( ||.(s . n).|| " ) * ||.(R /. (s . n)).||) by A19, ABSVALUE:def 1;

        ( dom R) = the carrier of S by A1, PARTFUN1:def 2;

        then

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

         ||.(((( ||.s.|| " ) (#) (R /* s)) . n) - ( 0. T)).|| = ||.((( ||.s.|| " ) (#) (R /* s)) . n).|| by RLVECT_1: 13

        .= ||.((( ||.s.|| " ) . n) * ((R /* s) . n)).|| by Def2

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

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

        .= ||.(( ||.(s . n).|| " ) * (R /. (s . n))).|| by A21, FUNCT_2: 109, A17;

        hence for r be Real st r > 0 holds ex d be Real st d > 0 & for z be Point of S st z <> ( 0. S) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r by A8, A18, A20;

      end;

      now

        assume

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

        now

          let s be ( 0. S) -convergent sequence of S such that

           A23: s is non-zero;

          

           A24: s is convergent & ( lim s) = ( 0. S) by Def4;

           A25:

          now

            let r be Real;

            assume r > 0 ;

            then

            consider d be Real such that

             A26: d > 0 and

             A27: for z be Point of S st z <> ( 0. S) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < r by A22;

            consider n be Nat such that

             A28: for m be Nat st n <= m holds ||.((s . m) - ( 0. S)).|| < d by A24, A26, NORMSP_1:def 7;

            take n;

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

            proof

              ( dom R) = the carrier of S by A1, PARTFUN1:def 2;

              then

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

              let m be Nat;

              

               A30: m in NAT by ORDINAL1:def 12;

              assume n <= m;

              then ||.((s . m) - ( 0. S)).|| < d by A28;

              then

               A31: ||.(s . m).|| < d by RLVECT_1: 13;

              

               A32: (s . m) <> ( 0. S) by Th7, A23;

              then ||.(s . m).|| <> 0 by NORMSP_0:def 5;

              then ||.(s . m).|| > 0 by NORMSP_1: 4;

              

              then (( ||.(s . m).|| " ) * ||.(R /. (s . m)).||) = ( |.( ||.(s . m).|| " ).| * ||.(R /. (s . m)).||) by ABSVALUE:def 1

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

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

              .= ||.((( ||.s.|| . m) " ) * ((R /* s) . m)).|| by NORMSP_0:def 4

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

              .= ||.((( ||.s.|| " ) (#) (R /* s)) . m).|| by Def2

              .= ||.(((( ||.s.|| " ) (#) (R /* s)) . m) - ( 0. T)).|| by RLVECT_1: 13;

              hence thesis by A27, A31, A32;

            end;

          end;

          hence (( ||.s.|| " ) (#) (R /* s)) is convergent;

          hence ( lim (( ||.s.|| " ) (#) (R /* s))) = ( 0. T) by A25, NORMSP_1:def 7;

        end;

        hence R is RestFunc-like by A1;

      end;

      hence thesis by A2;

    end;

    theorem :: NDIFF_1:24

    

     Th24: for R be RestFunc of S, T holds for s be ( 0. S) -convergent sequence of S st s is non-zero holds (R /* s) is convergent & ( lim (R /* s)) = ( 0. T)

    proof

      let R be RestFunc of S, T;

      let s be ( 0. S) -convergent sequence of S such that

       A1: s is non-zero;

      

       A2: (( ||.s.|| " ) (#) (R /* s)) is convergent by Def5, A1;

      now

        let n be Element of NAT ;

        (s . n) <> ( 0. S) by Th7, A1;

        then

         A3: ||.(s . n).|| <> 0 by NORMSP_0:def 5;

        

        thus (( ||.s.|| (#) (( ||.s.|| " ) (#) (R /* s))) . n) = (( ||.s.|| . n) * ((( ||.s.|| " ) (#) (R /* s)) . n)) by Def2

        .= (( ||.s.|| . n) * ((( ||.s.|| " ) . n) * ((R /* s) . n))) by Def2

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

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

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

        .= (( ||.(s . n).|| * ( ||.(s . n).|| " )) * ((R /* s) . n)) by RLVECT_1:def 7

        .= (1 * ((R /* s) . n)) by A3, XCMPLX_0:def 7

        .= ((R /* s) . n) by RLVECT_1:def 8;

      end;

      then

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

      

       A5: s is convergent by Def4;

      then

       A6: ||.s.|| is convergent by LOPBAN_1: 41;

      ( lim s) = ( 0. S) by Def4;

      then ( lim ||.s.||) = ||.( 0. S).|| by A5, LOPBAN_1: 41;

      then

       A7: ( lim ||.s.||) = 0 by NORMSP_1: 1;

      ( lim (( ||.s.|| " ) (#) (R /* s))) = ( 0. T) by Def5, A1;

      then ( lim (R /* s)) = ( 0 * ( 0. T)) by A5, A4, A2, A7, Th14, LOPBAN_1: 41;

      hence thesis by A4, A2, A6, Th13, RLVECT_1: 10;

    end;

    reserve R,R1,R2 for RestFunc of S, T;

    reserve L,L1,L2 for Point of ( R_NormSpace_of_BoundedLinearOperators (S,T));

    theorem :: NDIFF_1:25

    

     Th25: for h1,h2 be PartFunc of S, T holds for seq be sequence of S holds h1 is total & h2 is total implies ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq))

    proof

      let h1,h2 be PartFunc of S, T;

      let seq be sequence of S;

      assume h1 is total & h2 is total;

      then (h1 + h2) is total by VFUNCT_1: 32;

      then ( dom (h1 + h2)) = the carrier of S by PARTFUN1:def 2;

      then (( dom h1) /\ ( dom h2)) = the carrier of S by VFUNCT_1:def 1;

      then

       A1: ( rng seq) c= (( dom h1) /\ ( dom h2));

      hence ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) by NFCONT_1: 12;

      thus thesis by A1, NFCONT_1: 12;

    end;

    theorem :: NDIFF_1:26

    

     Th26: for h be PartFunc of S, T holds for seq be sequence of S holds for r be Real holds h is total implies ((r (#) h) /* seq) = (r * (h /* seq))

    proof

      let h be PartFunc of S, T;

      let seq be sequence of S;

      let r be Real;

      assume h is total;

      then ( dom h) = the carrier of S by PARTFUN1:def 2;

      then ( rng seq) c= ( dom h);

      hence thesis by NFCONT_1: 13;

    end;

    theorem :: NDIFF_1:27

    

     Th27: f is_continuous_in x0 iff x0 in ( dom f) & for s1 be sequence of S st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n be Nat holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1))

    proof

      thus f is_continuous_in x0 implies x0 in ( dom f) & for s1 be sequence of S st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n be Nat holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

      assume that

       A1: x0 in ( dom f) and

       A2: for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n be Nat holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

      thus x0 in ( dom f) by A1;

      let s2 be sequence of S such that

       A3: ( rng s2) c= ( dom f) and

       A4: s2 is convergent & ( lim s2) = x0;

      now

        per cases ;

          suppose ex n st for m be Element of NAT st n <= m holds (s2 . m) = x0;

          then

          consider N be Element of NAT such that

           A5: for m be Element of NAT st N <= m holds (s2 . m) = x0;

          

           A6: for n holds ((s2 ^\ N) . n) = x0

          proof

            let n;

            (s2 . (n + N)) = x0 by A5, NAT_1: 12;

            hence thesis by NAT_1:def 3;

          end;

          

           A7: ( rng (s2 ^\ N)) c= ( rng s2) by VALUED_0: 21;

           A8:

          now

            let p be Real such that

             A9: p > 0 ;

            reconsider n = 0 as Nat;

            take n;

            let m be Nat such that n <= m;

            

             A10: m in NAT by ORDINAL1:def 12;

             ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A3, A7, FUNCT_2: 109, XBOOLE_1: 1, A10

            .= ||.((f /. x0) - (f /. x0)).|| by A6, A10

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

            .= 0 by NORMSP_1: 1;

            hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A9;

          end;

          then

           A11: (f /* (s2 ^\ N)) is convergent;

          

           A12: (f /* (s2 ^\ N)) = ((f /* s2) ^\ N) by A3, VALUED_0: 27;

          then

           A13: (f /* s2) is convergent by A11, LOPBAN_3: 10;

          (f /. x0) = ( lim ((f /* s2) ^\ N)) by A8, A11, A12, NORMSP_1:def 7;

          hence thesis by A13, LOPBAN_3: 9;

        end;

          suppose

           A14: for n holds ex m be Element of NAT st n <= m & (s2 . m) <> x0;

          defpred P[ Nat, set, set] means for n,m be Element of NAT st $2 = n & $3 = m holds n < m & (s2 . m) <> x0 & for k st n < k & (s2 . k) <> x0 holds m <= k;

          defpred P[ Nat] means (s2 . $1) <> x0;

          ex m1 be Element of NAT st 0 <= m1 & (s2 . m1) <> x0 by A14;

          then

           A15: ex m be Nat st P[m];

          consider M be Nat such that

           A16: P[M] & for n be Nat st P[n] holds M <= n from NAT_1:sch 5( A15);

          reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

           A17:

          now

            let n;

            consider m be Element of NAT such that

             A18: (n + 1) <= m & (s2 . m) <> x0 by A14;

            take m;

            thus n < m & (s2 . m) <> x0 by A18, NAT_1: 13;

          end;

          

           A19: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st P[n, x, y]

          proof

            let n be Nat;

            let x be Element of NAT ;

            defpred P[ Nat] means x < $1 & (s2 . $1) <> x0;

            ex m be Element of NAT st P[m] by A17;

            then

             A20: ex m be Nat st P[m];

            consider l be Nat such that

             A21: P[l] & for k be Nat st P[k] holds l <= k from NAT_1:sch 5( A20);

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

            take l;

            thus thesis by A21;

          end;

          consider F be sequence of NAT such that

           A22: (F . 0 ) = M9 & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A19);

          

           A23: ( rng F) c= REAL by NUMBERS: 19;

          

           A24: ( rng F) c= NAT ;

          

           A25: ( dom F) = NAT by FUNCT_2:def 1;

          then

          reconsider F as Real_Sequence by A23, RELSET_1: 4;

           A26:

          now

            let n;

            (F . n) in ( rng F) by A25, FUNCT_1:def 3;

            hence (F . n) is Element of NAT by A24;

          end;

          now

            let n be Nat;

            

             A27: n in NAT by ORDINAL1:def 12;

            (F . n) is Element of NAT & (F . (n + 1)) is Element of NAT by A26, A27;

            hence (F . n) < (F . (n + 1)) by A22;

          end;

          then

          reconsider F as increasing sequence of NAT by SEQM_3:def 6;

          

           A28: (s2 * F) is convergent & ( lim (s2 * F)) = x0 by A4, LOPBAN_3: 7, LOPBAN_3: 8;

          

           A29: for n st (s2 . n) <> x0 holds ex m be Element of NAT st (F . m) = n

          proof

            defpred P[ Nat] means (s2 . $1) <> x0 & for m be Element of NAT holds (F . m) <> $1;

            assume ex n st P[n];

            then

             A30: ex n be Nat st P[n];

            consider M1 be Nat such that

             A31: P[M1] & for n be Nat st P[n] holds M1 <= n from NAT_1:sch 5( A30);

            defpred P[ Nat] means $1 < M1 & (s2 . $1) <> x0 & ex m be Element of NAT st (F . m) = $1;

            

             A32: ex n be Nat st P[n]

            proof

              take M;

              M <= M1 & M <> M1 by A16, A22, A31;

              hence M < M1 by XXREAL_0: 1;

              thus (s2 . M) <> x0 by A16;

              take 0 ;

              thus thesis by A22;

            end;

            

             A33: for n be Nat st P[n] holds n <= M1;

            consider MX be Nat such that

             A34: P[MX] & for n be Nat st P[n] holds n <= MX from NAT_1:sch 6( A33, A32);

            

             A35: for k st MX < k & k < M1 holds (s2 . k) = x0

            proof

              given k such that

               A36: MX < k and

               A37: k < M1 & (s2 . k) <> x0;

              now

                per cases ;

                  suppose ex m be Element of NAT st (F . m) = k;

                  hence contradiction by A34, A36, A37;

                end;

                  suppose for m be Element of NAT holds (F . m) <> k;

                  hence contradiction by A31, A37;

                end;

              end;

              hence contradiction;

            end;

            consider m be Element of NAT such that

             A38: (F . m) = MX by A34;

            

             A39: MX < (F . (m + 1)) & (s2 . (F . (m + 1))) <> x0 by A22, A38;

            M1 in NAT by ORDINAL1:def 12;

            then

             A40: (F . (m + 1)) <= M1 by A22, A31, A34, A38;

            now

              assume (F . (m + 1)) <> M1;

              then (F . (m + 1)) < M1 by A40, XXREAL_0: 1;

              hence contradiction by A35, A39;

            end;

            hence contradiction by A31;

          end;

          

           A41: for n be Nat holds ((s2 * F) . n) <> x0

          proof

            defpred P[ Nat] means ((s2 * F) . $1) <> x0;

            

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

            proof

              let k be Nat such that ((s2 * F) . k) <> x0;

               P[k, (F . k), (F . (k + 1))] by A22;

              then (s2 . (F . (k + 1))) <> x0;

              hence thesis by FUNCT_2: 15;

            end;

            

             A43: P[ 0 ] by A16, A22, FUNCT_2: 15;

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

          end;

          

           A44: ( rng (s2 * F)) c= ( rng s2) by VALUED_0: 21;

          then ( rng (s2 * F)) c= ( dom f) by A3;

          then

           A45: (f /* (s2 * F)) is convergent & (f /. x0) = ( lim (f /* (s2 * F))) by A2, A41, A28;

           A46:

          now

            let p be Real;

            assume

             A47: 0 < p;

            then

            consider n be Nat such that

             A48: for m be Nat st n <= m holds ||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A45, NORMSP_1:def 7;

            reconsider k = (F . n) as Nat;

            take k;

            let m be Nat such that

             A49: k <= m;

            

             A50: m in NAT by ORDINAL1:def 12;

            now

              per cases ;

                suppose

                 A51: (s2 . m) = x0;

                 ||.(((f /* s2) . m) - (f /. x0)).|| = ||.((f /. (s2 . m)) - (f /. x0)).|| by A3, FUNCT_2: 109, A50

                .= ||.( 0. T).|| by A51, RLVECT_1: 15

                .= 0 by NORMSP_1: 1;

                hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A47;

              end;

                suppose (s2 . m) <> x0;

                then

                consider l be Element of NAT such that

                 A52: m = (F . l) by A29, A50;

                n <= l by A49, A52, SEQM_3: 1;

                then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A48;

                then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A3, A44, FUNCT_2: 109, XBOOLE_1: 1;

                then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A52, FUNCT_2: 15;

                hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A3, FUNCT_2: 109, A50;

              end;

            end;

            hence ||.(((f /* s2) . m) - (f /. x0)).|| < p;

          end;

          hence (f /* s2) is convergent;

          hence (f /. x0) = ( lim (f /* s2)) by A46, NORMSP_1:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_1:28

    

     Th28: for R1, R2 holds (R1 + R2) is RestFunc of S, T & (R1 - R2) is RestFunc of S, T

    proof

      let R1, R2;

      

       A1: R1 is total & R2 is total by Def5;

       A2:

      now

        let h;

        assume

         A3: h is non-zero;

        

         A4: (( ||.h.|| " ) (#) (R1 /* h)) is convergent & (( ||.h.|| " ) (#) (R2 /* h)) is convergent by Def5, A3;

        

         A5: (( ||.h.|| " ) (#) ((R1 + R2) /* h)) = (( ||.h.|| " ) (#) ((R1 /* h) + (R2 /* h))) by A1, Th25

        .= ((( ||.h.|| " ) (#) (R1 /* h)) + (( ||.h.|| " ) (#) (R2 /* h))) by Th9;

        hence (( ||.h.|| " ) (#) ((R1 + R2) /* h)) is convergent by A4, NORMSP_1: 19;

        ( lim (( ||.h.|| " ) (#) (R1 /* h))) = ( 0. T) & ( lim (( ||.h.|| " ) (#) (R2 /* h))) = ( 0. T) by A3, Def5;

        

        hence ( lim (( ||.h.|| " ) (#) ((R1 + R2) /* h))) = (( 0. T) + ( 0. T)) by A4, A5, NORMSP_1: 25

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

      end;

       A6:

      now

        let h;

        assume

         A7: h is non-zero;

        

         A8: (( ||.h.|| " ) (#) (R1 /* h)) is convergent & (( ||.h.|| " ) (#) (R2 /* h)) is convergent by Def5, A7;

        

         A9: (( ||.h.|| " ) (#) ((R1 - R2) /* h)) = (( ||.h.|| " ) (#) ((R1 /* h) - (R2 /* h))) by A1, Th25

        .= ((( ||.h.|| " ) (#) (R1 /* h)) - (( ||.h.|| " ) (#) (R2 /* h))) by Th12;

        hence (( ||.h.|| " ) (#) ((R1 - R2) /* h)) is convergent by A8, NORMSP_1: 20;

        ( lim (( ||.h.|| " ) (#) (R1 /* h))) = ( 0. T) & ( lim (( ||.h.|| " ) (#) (R2 /* h))) = ( 0. T) by Def5, A7;

        

        hence ( lim (( ||.h.|| " ) (#) ((R1 - R2) /* h))) = (( 0. T) - ( 0. T)) by A8, A9, NORMSP_1: 26

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

      end;

      (R1 + R2) is total by A1, VFUNCT_1: 32;

      hence (R1 + R2) is RestFunc of S, T by A2, Def5;

      (R1 - R2) is total by A1, VFUNCT_1: 32;

      hence thesis by A6, Def5;

    end;

    theorem :: NDIFF_1:29

    

     Th29: for r, R holds (r (#) R) is RestFunc of S, T

    proof

      let r, R;

      

       A1: R is total by Def5;

       A2:

      now

        let h;

        assume

         A3: h is non-zero;

        

         A4: (( ||.h.|| " ) (#) (R /* h)) is convergent by A3, Def5;

        

         A5: (( ||.h.|| " ) (#) ((r (#) R) /* h)) = (( ||.h.|| " ) (#) (r * (R /* h))) by A1, Th26

        .= (r * (( ||.h.|| " ) (#) (R /* h))) by Th10;

        hence (( ||.h.|| " ) (#) ((r (#) R) /* h)) is convergent by A4, NORMSP_1: 22;

        ( lim (( ||.h.|| " ) (#) (R /* h))) = ( 0. T) by A3, Def5;

        

        hence ( lim (( ||.h.|| " ) (#) ((r (#) R) /* h))) = (r * ( 0. T)) by A4, A5, NORMSP_1: 28

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

      end;

      (r (#) R) is total by A1, VFUNCT_1: 34;

      hence thesis by A2, Def5;

    end;

    definition

      let S, T;

      let f be PartFunc of S, T;

      let x0 be Point of S;

      :: NDIFF_1:def6

      pred f is_differentiable_in x0 means ex N be Neighbourhood of x0 st N c= ( dom f) & ex L, R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

    end

    definition

      let S, T;

      let f be PartFunc of S, T;

      let x0 be Point of S;

      assume

       A1: f is_differentiable_in x0;

      :: NDIFF_1:def7

      func diff (f,x0) -> Point of ( R_NormSpace_of_BoundedLinearOperators (S,T)) means

      : Def7: ex N be Neighbourhood of x0 st N c= ( dom f) & ex R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((it . (x - x0)) + (R /. (x - x0)));

      existence by A1;

      uniqueness

      proof

        let LB,LB1 be Point of ( R_NormSpace_of_BoundedLinearOperators (S,T));

        

         A2: ( R_NormSpace_of_BoundedLinearOperators (S,T)) = NORMSTR (# ( BoundedLinearOperators (S,T)), ( Zero_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Add_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Mult_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;

        then

        reconsider L = LB as Element of ( BoundedLinearOperators (S,T));

        reconsider L1 = LB1 as Element of ( BoundedLinearOperators (S,T)) by A2;

        assume that

         A3: ex N be Neighbourhood of x0 st N c= ( dom f) & ex R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((LB . (x - x0)) + (R /. (x - x0))) and

         A4: ex N be Neighbourhood of x0 st N c= ( dom f) & ex R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((LB1 . (x - x0)) + (R /. (x - x0)));

        consider N be Neighbourhood of x0 such that N c= ( dom f) and

         A5: ex R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((LB . (x - x0)) + (R /. (x - x0))) by A3;

        consider R such that

         A6: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((LB . (x - x0)) + (R /. (x - x0))) by A5;

        consider N1 be Neighbourhood of x0 such that N1 c= ( dom f) and

         A7: ex R st for x be Point of S st x in N1 holds ((f /. x) - (f /. x0)) = ((LB1 . (x - x0)) + (R /. (x - x0))) by A4;

        consider R1 such that

         A8: for x be Point of S st x in N1 holds ((f /. x) - (f /. x0)) = ((LB1 . (x - x0)) + (R1 /. (x - x0))) by A7;

        

         A9: for z be Point of S holds (( modetrans (L,S,T)) . z) = (( modetrans (L1,S,T)) . z)

        proof

          let z be Point of S;

          now

            per cases ;

              case

               A10: z = ( 0. S);

              

              hence (( modetrans (L,S,T)) . z) = (( modetrans (L,S,T)) . ( 0 * z)) by RLVECT_1: 10

              .= ( 0 * (( modetrans (L,S,T)) . z)) by LOPBAN_1:def 5

              .= ( 0. T) by RLVECT_1: 10

              .= ( 0 * (( modetrans (L1,S,T)) . z)) by RLVECT_1: 10

              .= (( modetrans (L1,S,T)) . ( 0 * z)) by LOPBAN_1:def 5

              .= (( modetrans (L1,S,T)) . z) by A10, RLVECT_1: 10;

            end;

              case

               A11: z <> ( 0. S);

              consider N0 be Neighbourhood of x0 such that

               A12: N0 c= N & N0 c= N1 by Th1;

              consider g be Real such that

               A13: 0 < g and

               A14: { y where y be Point of S : ||.(y - x0).|| < g } c= N0 by NFCONT_1:def 1;

              consider n0 be Nat such that

               A15: ( ||.z.|| / g) < n0 by SEQ_4: 3;

              set n1 = (n0 + 1);

              n0 <= (n0 + 1) by NAT_1: 11;

              then ( ||.z.|| / g) < (n0 + 1) by A15, XXREAL_0: 2;

              then (( ||.z.|| / g) * g) < ((n0 + 1) * g) by A13, XREAL_1: 68;

              then ||.z.|| < ((n0 + 1) * g) by A13, XCMPLX_1: 87;

              then

               A16: ( ||.z.|| / (n0 + 1)) < g by XREAL_1: 83;

              ex r be Real_Sequence st (for n be Element of NAT holds ((r . n) = (1 / (n + n1)) & (r . n) > 0 & (((r . n) * z) + x0) in N0)) & r is convergent & ( lim r) = 0

              proof

                deffunc F( Nat) = (1 / ($1 + n1));

                consider r be Real_Sequence such that

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

                take r;

                thus for n be Element of NAT holds (r . n) = (1 / (n + n1)) & (r . n) > 0 & (((r . n) * z) + x0) in N0

                proof

                  let n be Element of NAT ;

                  thus (r . n) = (1 / (n + n1)) by A17;

                  n1 <= (n + n1) & 0 <= ||.z.|| by NAT_1: 12, NORMSP_1: 4;

                  then

                   A18: ( ||.z.|| / (n + n1)) <= ( ||.z.|| / n1) by XREAL_1: 118;

                   0 < (1 * ((n + n1) " ));

                  then 0 < (1 / (n + n1)) by XCMPLX_0:def 9;

                  hence (r . n) > 0 by A17;

                   ||.((((r . n) * z) + x0) - x0).|| = ||.(((r . n) * z) + (x0 - x0)).|| by RLVECT_1:def 3

                  .= ||.(((r . n) * z) + ( 0. S)).|| by RLVECT_1: 15

                  .= ||.((r . n) * z).|| by RLVECT_1: 4

                  .= ||.((1 / (n + n1)) * z).|| by A17

                  .= ( |.(1 / (n + n1)).| * ||.z.||) by NORMSP_1:def 1

                  .= ((1 / (n + n1)) * ||.z.||) by ABSVALUE:def 1

                  .= ( ||.z.|| / (n + n1)) by XCMPLX_1: 99;

                  then ||.((((r . n) * z) + x0) - x0).|| < g by A16, A18, XXREAL_0: 2;

                  then (((r . n) * z) + x0) in { y where y be Point of S : ||.(y - x0).|| < g };

                  hence thesis by A14;

                end;

                thus thesis by A17, SEQ_4: 31;

              end;

              then

              consider r be Real_Sequence such that

               A19: for n be Element of NAT holds (r . n) = (1 / (n + n1)) & (r . n) > 0 & (((r . n) * z) + x0) in N0 and r is convergent and ( lim r) = 0 ;

              deffunc F( Element of NAT ) = ((r . $1) * z);

              consider s be sequence of S such that

               A20: for n holds (s . n) = F(n) from FUNCT_2:sch 4;

              now

                let n be Nat;

                

                 A21: n in NAT by ORDINAL1:def 12;

                assume (s . n) = ( 0. S);

                then ((r . n) * z) = ( 0. S) by A20, A21;

                then (r . n) = 0 or z = ( 0. S) by RLVECT_1: 11;

                hence contradiction by A11, A19, A21;

              end;

              then

               A22: s is non-zero by Th7;

              now

                let n be Nat;

                

                 A23: n in NAT by ORDINAL1:def 12;

                

                hence (s . n) = ((r . n) * z) by A20

                .= ((1 / (n + n1)) * z) by A19, A23;

              end;

              then s is convergent & ( lim s) = ( 0. S) by Th19, Th20;

              then

              reconsider s as ( 0. S) -convergent sequence of S by Def4;

               A24:

              now

                let x be Point of S;

                assume that

                 A25: x in N and

                 A26: x in N1;

                ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A6, A25;

                hence ((L . (x - x0)) + (R /. (x - x0))) = ((L1 . (x - x0)) + (R1 /. (x - x0))) by A8, A26;

              end;

              now

                R1 is total by Def5;

                then ( dom R1) = the carrier of S by PARTFUN1:def 2;

                then

                 A27: ( rng s) c= ( dom R1);

                R is total by Def5;

                then ( dom R) = the carrier of S by PARTFUN1:def 2;

                then

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

                let n be Nat;

                set x = (((r . n) * z) + x0);

                

                 A29: (x - x0) = (((r . n) * z) + (x0 - x0)) by RLVECT_1:def 3

                .= (((r . n) * z) + ( 0. S)) by RLVECT_1: 15

                .= ((r . n) * z) by RLVECT_1: 4;

                

                 A30: n in NAT by ORDINAL1:def 12;

                then

                 A31: (r . n) <> 0 by A19;

                (s . n) <> ( 0. S) by A22, Th7;

                then

                 A32: ||.(s . n).|| <> 0 by NORMSP_0:def 5;

                

                 A33: (r . n) > 0 by A19, A30;

                 ||.(s . n).|| = ||.((r . n) * z).|| by A20, A30

                .= ( |.(r . n).| * ||.z.||) by NORMSP_1:def 1

                .= ((r . n) * ||.z.||) by A33, ABSVALUE:def 1;

                

                then (((r . n) " ) * ||.(s . n).||) = ((((r . n) " ) * (r . n)) * ||.z.||)

                .= (((r . n) / (r . n)) * ||.z.||) by XCMPLX_0:def 9

                .= (1 * ||.z.||) by A31, XCMPLX_1: 60

                .= ||.z.||;

                

                then ( ||.z.|| * ( ||.(s . n).|| " )) = (((r . n) " ) * ( ||.(s . n).|| * ( ||.(s . n).|| " )))

                .= (((r . n) " ) * ( ||.(s . n).|| / ||.(s . n).||)) by XCMPLX_0:def 9

                .= (((r . n) " ) * 1) by A32, XCMPLX_1: 60

                .= ((r . n) " );

                then

                 A34: ( ||.z.|| * (( ||.s.|| . n) " )) = ((r . n) " ) by NORMSP_0:def 4;

                x in N0 by A19, A30;

                then ((L . ((r . n) * z)) + (R /. ((r . n) * z))) = ((L1 . ((r . n) * z)) + (R1 /. ((r . n) * z))) by A24, A12, A29;

                then

                 A35: ((((r . n) " ) * (L . ((r . n) * z))) + (((r . n) " ) * (R /. ((r . n) * z)))) = (((r . n) " ) * ((L1 . ((r . n) * z)) + (R1 /. ((r . n) * z)))) by RLVECT_1:def 5;

                

                 A36: (((r . n) " ) * (L1 . ((r . n) * z))) = (((r . n) " ) * (( modetrans (L1,S,T)) . ((r . n) * z))) by LOPBAN_1:def 11

                .= (((r . n) " ) * ((r . n) * (( modetrans (L1,S,T)) . z))) by LOPBAN_1:def 5

                .= (((r . n) " ) * ((r . n) * (L1 . z))) by LOPBAN_1:def 11

                .= ((((r . n) " ) * (r . n)) * (L1 . z)) by RLVECT_1:def 7

                .= (((r . n) / (r . n)) * (L1 . z)) by XCMPLX_0:def 9

                .= (1 * (L1 . z)) by A31, XCMPLX_1: 60

                .= (L1 . z) by RLVECT_1:def 8;

                (((r . n) " ) * (L . ((r . n) * z))) = (((r . n) " ) * (( modetrans (L,S,T)) . ((r . n) * z))) by LOPBAN_1:def 11

                .= (((r . n) " ) * ((r . n) * (( modetrans (L,S,T)) . z))) by LOPBAN_1:def 5

                .= (((r . n) " ) * ((r . n) * (L . z))) by LOPBAN_1:def 11

                .= ((((r . n) " ) * (r . n)) * (L . z)) by RLVECT_1:def 7

                .= (((r . n) / (r . n)) * (L . z)) by XCMPLX_0:def 9

                .= (1 * (L . z)) by A31, XCMPLX_1: 60

                .= (L . z) by RLVECT_1:def 8;

                then

                 A37: ((L . z) + (((r . n) " ) * (R /. ((r . n) * z)))) = ((L1 . z) + (((r . n) " ) * (R1 /. ((r . n) * z)))) by A35, A36, RLVECT_1:def 5;

                

                 A38: (((r . n) " ) * (R1 /. ((r . n) * z))) = (((r . n) " ) * (R1 /. (s . n))) by A20, A30

                .= (( ||.z.|| * (( ||.s.|| " ) . n)) * (R1 /. (s . n))) by A34, VALUED_1: 10

                .= ( ||.z.|| * ((( ||.s.|| " ) . n) * (R1 /. (s . n)))) by RLVECT_1:def 7

                .= ( ||.z.|| * ((( ||.s.|| " ) . n) * ((R1 /* s) . n))) by A30, A27, FUNCT_2: 109

                .= ( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n)) by Def2;

                (((r . n) " ) * (R /. ((r . n) * z))) = (((r . n) " ) * (R /. (s . n))) by A20, A30

                .= (( ||.z.|| * (( ||.s.|| " ) . n)) * (R /. (s . n))) by A34, VALUED_1: 10

                .= ( ||.z.|| * ((( ||.s.|| " ) . n) * (R /. (s . n)))) by RLVECT_1:def 7

                .= ( ||.z.|| * ((( ||.s.|| " ) . n) * ((R /* s) . n))) by A30, A28, FUNCT_2: 109

                .= ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n)) by Def2;

                then ((L . z) + (( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n)) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n)))) = (((L1 . z) + ( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n))) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n))) by A37, A38, RLVECT_1:def 3;

                then ((L . z) + ( 0. T)) = (((L1 . z) + ( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n))) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n))) by RLVECT_1: 15;

                then (L . z) = (((L1 . z) + ( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n))) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n))) by RLVECT_1:def 4;

                then ((L . z) - (L1 . z)) = (( - (L1 . z)) + ((L1 . z) + (( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n)) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n))))) by RLVECT_1:def 3;

                then ((L . z) - (L1 . z)) = ((( - (L1 . z)) + (L1 . z)) + (( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n)) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n)))) by RLVECT_1:def 3;

                then ((L . z) - (L1 . z)) = (( 0. T) + (( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n)) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n)))) by RLVECT_1: 5;

                then ((L . z) - (L1 . z)) = (( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) . n)) - ( ||.z.|| * ((( ||.s.|| " ) (#) (R /* s)) . n))) by RLVECT_1: 4;

                then ((L . z) - (L1 . z)) = ( ||.z.|| * (((( ||.s.|| " ) (#) (R1 /* s)) . n) - ((( ||.s.|| " ) (#) (R /* s)) . n))) by RLVECT_1: 34;

                then ((L . z) - (L1 . z)) = ( ||.z.|| * (((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s))) . n)) by NORMSP_1:def 3;

                hence ((L . z) - (L1 . z)) = (( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s)))) . n) by NORMSP_1:def 5;

              end;

              then ( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s)))) is constant & (( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s)))) . 1) = ((L . z) - (L1 . z)) by VALUED_0:def 18;

              then

               A39: ( lim ( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s))))) = ((L . z) - (L1 . z)) by Th18;

              

               A40: (( ||.s.|| " ) (#) (R /* s)) is convergent & (( ||.s.|| " ) (#) (R1 /* s)) is convergent by A22, Def5;

              ( lim (( ||.s.|| " ) (#) (R /* s))) = ( 0. T) & ( lim (( ||.s.|| " ) (#) (R1 /* s))) = ( 0. T) by A22, Def5;

              

              then

               A41: ( lim ((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s)))) = (( 0. T) - ( 0. T)) by A40, NORMSP_1: 26

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

              

               A42: ( lim ( ||.z.|| * ((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s))))) = ( ||.z.|| * ( lim ((( ||.s.|| " ) (#) (R1 /* s)) - (( ||.s.|| " ) (#) (R /* s))))) by A40, NORMSP_1: 20, NORMSP_1: 28

              .= ( 0. T) by A41, RLVECT_1: 10;

              

              thus (( modetrans (L,S,T)) . z) = (L . z) by LOPBAN_1:def 11

              .= (L1 . z) by A39, A42, RLVECT_1: 21

              .= (( modetrans (L1,S,T)) . z) by LOPBAN_1:def 11;

            end;

          end;

          hence thesis;

        end;

        

        thus LB = ( modetrans (L,S,T)) by LOPBAN_1:def 11

        .= ( modetrans (L1,S,T)) by A9, FUNCT_2: 63

        .= LB1 by LOPBAN_1:def 11;

      end;

    end

    definition

      let X;

      let S, T;

      let f be PartFunc of S, T;

      :: NDIFF_1:def8

      pred f is_differentiable_on X means X c= ( dom f) & for x be Point of S st x in X holds (f | X) is_differentiable_in x;

    end

    theorem :: NDIFF_1:30

    

     Th30: for f be PartFunc of S, T holds (f is_differentiable_on X implies X is Subset of S) by XBOOLE_1: 1;

    theorem :: NDIFF_1:31

    

     Th31: for f be PartFunc of S, T holds for Z be Subset of S st Z is open holds (f is_differentiable_on Z iff Z c= ( dom f) & for x be Point of S st x in Z holds f is_differentiable_in x)

    proof

      let f be PartFunc of S, T;

      let Z be Subset of S such that

       A1: Z is open;

      thus f is_differentiable_on Z implies Z c= ( dom f) & for x be Point of S st x in Z holds f is_differentiable_in x

      proof

        assume

         A2: f is_differentiable_on Z;

        hence

         A3: Z c= ( dom f);

        let x0 be Point of S;

        assume

         A4: x0 in Z;

        then (f | Z) is_differentiable_in x0 by A2;

        then

        consider N be Neighbourhood of x0 such that

         A5: N c= ( dom (f | Z)) and

         A6: ex L, R st for x be Point of S st x in N holds (((f | Z) /. x) - ((f | Z) /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

        consider L, R such that

         A7: for x be Point of S st x in N holds (((f | Z) /. x) - ((f | Z) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A6;

        take N;

        

         A8: ( dom (f | Z)) = (( dom f) /\ Z) by RELAT_1: 61;

        then ( dom (f | Z)) c= ( dom f) by XBOOLE_1: 17;

        hence N c= ( dom f) by A5;

        take L, R;

        let x be Point of S;

        assume

         A9: x in N;

        then (((f | Z) /. x) - ((f | Z) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A7;

        then ((f /. x) - ((f | Z) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A5, A8, A9, PARTFUN2: 16;

        hence thesis by A3, A4, PARTFUN2: 17;

      end;

      assume that

       A10: Z c= ( dom f) and

       A11: for x be Point of S st x in Z holds f is_differentiable_in x;

      thus Z c= ( dom f) by A10;

      let x0 be Point of S;

      assume

       A12: x0 in Z;

      then

      consider N1 be Neighbourhood of x0 such that

       A13: N1 c= Z by A1, Th2;

      f is_differentiable_in x0 by A11, A12;

      then

      consider N be Neighbourhood of x0 such that

       A14: N c= ( dom f) and

       A15: ex L, R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

      consider N2 be Neighbourhood of x0 such that

       A16: N2 c= N1 and

       A17: N2 c= N by Th1;

      

       A18: N2 c= Z by A13, A16;

      take N2;

      N2 c= ( dom f) by A14, A17;

      then

       A19: N2 c= (( dom f) /\ Z) by A18, XBOOLE_1: 19;

      hence N2 c= ( dom (f | Z)) by RELAT_1: 61;

      

       A20: x0 in N2 by NFCONT_1: 4;

      consider L, R such that

       A21: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A15;

      take L, R;

      let x be Point of S;

      assume

       A22: x in N2;

      then ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A17, A21;

      then (((f | Z) /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A19, A22, PARTFUN2: 16;

      hence thesis by A19, A20, PARTFUN2: 16;

    end;

    theorem :: NDIFF_1:32

    for f be PartFunc of S, T holds for Y be Subset of S holds f is_differentiable_on Y implies Y is open

    proof

      let f be PartFunc of S, T;

      let Y be Subset of S;

      assume

       A1: f is_differentiable_on Y;

      now

        let x0 be Point of S;

        assume x0 in Y;

        then (f | Y) is_differentiable_in x0 by A1;

        then

        consider N be Neighbourhood of x0 such that

         A2: N c= ( dom (f | Y)) and ex L, R st for x be Point of S st x in N holds (((f | Y) /. x) - ((f | Y) /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

        take N;

        ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61;

        then ( dom (f | Y)) c= Y by XBOOLE_1: 17;

        hence N c= Y by A2;

      end;

      hence thesis by Th4;

    end;

    definition

      let S, T;

      let f be PartFunc of S, T;

      let X be set;

      assume

       A1: f is_differentiable_on X;

      :: NDIFF_1:def9

      func f `| X -> PartFunc of S, ( R_NormSpace_of_BoundedLinearOperators (S,T)) means

      : Def9: ( dom it ) = X & for x be Point of S st x in X holds (it /. x) = ( diff (f,x));

      existence

      proof

        deffunc F( Point of S) = ( diff (f,$1));

        defpred P[ Point of S] means $1 in X;

        consider F be PartFunc of S, ( R_NormSpace_of_BoundedLinearOperators (S,T)) such that

         A2: (for x be Point of S holds x in ( dom F) iff P[x]) & for x be Point of S st x in ( dom F) holds (F . x) = F(x) from SEQ_1:sch 3;

        take F;

        now

          

           A3: X is Subset of S by A1, Th30;

          let y be object;

          assume y in X;

          hence y in ( dom F) by A2, A3;

        end;

        then

         A4: X c= ( dom F);

        for y be object st y in ( dom F) holds y in X by A2;

        then ( dom F) c= X;

        hence ( dom F) = X by A4;

        now

          let x be Point of S;

          assume x in X;

          then

           A5: x in ( dom F) by A2;

          then (F . x) = ( diff (f,x)) by A2;

          hence (F /. x) = ( diff (f,x)) by A5, PARTFUN1:def 6;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be PartFunc of S, ( R_NormSpace_of_BoundedLinearOperators (S,T));

        assume that

         A6: ( dom F) = X and

         A7: for x be Point of S st x in X holds (F /. x) = ( diff (f,x)) and

         A8: ( dom G) = X and

         A9: for x be Point of S st x in X holds (G /. x) = ( diff (f,x));

        now

          let x be Point of S;

          assume

           A10: x in ( dom F);

          then (F /. x) = ( diff (f,x)) by A6, A7;

          hence (F /. x) = (G /. x) by A6, A9, A10;

        end;

        hence thesis by A6, A8, PARTFUN2: 1;

      end;

    end

    theorem :: NDIFF_1:33

    for f be PartFunc of S, T holds for Z be Subset of S st Z is open & Z c= ( dom f) & ex r be Point of T st ( rng f) = {r} holds f is_differentiable_on Z & for x be Point of S st x in Z holds ((f `| Z) /. x) = ( 0. ( R_NormSpace_of_BoundedLinearOperators (S,T)))

    proof

      let f be PartFunc of S, T;

      let Z be Subset of S such that

       A1: Z is open and

       A2: Z c= ( dom f);

      reconsider R = (the carrier of S --> ( 0. T)) as PartFunc of S, T;

      set L = ( 0. ( R_NormSpace_of_BoundedLinearOperators (S,T)));

      given r be Point of T such that

       A3: ( rng f) = {r};

      ( R_NormSpace_of_BoundedLinearOperators (S,T)) = NORMSTR (# ( BoundedLinearOperators (S,T)), ( Zero_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Add_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Mult_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;

      then

      reconsider L as Element of ( BoundedLinearOperators (S,T));

      

       A4: ( dom R) = the carrier of S;

       A5:

      now

        let h;

        assume h is non-zero;

         A6:

        now

          let n be Nat;

          

           A7: (R /. (h . n)) = (R . (h . n)) by A4, PARTFUN1:def 6

          .= ( 0. T);

          

           A8: ( rng h) c= ( dom R);

          

           A9: n in NAT by ORDINAL1:def 12;

          

          thus ((( ||.h.|| " ) (#) (R /* h)) . n) = ((( ||.h.|| " ) . n) * ((R /* h) . n)) by Def2

          .= ((( ||.h.|| " ) . n) * (R /. (h . n))) by A9, A8, FUNCT_2: 109

          .= ( 0. T) by A7, RLVECT_1: 10;

        end;

        then

         A10: (( ||.h.|| " ) (#) (R /* h)) is constant by VALUED_0:def 18;

        hence (( ||.h.|| " ) (#) (R /* h)) is convergent by Th18;

        ((( ||.h.|| " ) (#) (R /* h)) . 0 ) = ( 0. T) by A6;

        hence ( lim (( ||.h.|| " ) (#) (R /* h))) = ( 0. T) by A10, Th18;

      end;

       A11:

      now

        let x0 be Point of S;

        assume

         A12: x0 in ( dom f);

        then (f . x0) in {r} by A3, FUNCT_1:def 3;

        then (f /. x0) in {r} by A12, PARTFUN1:def 6;

        hence (f /. x0) = r by TARSKI:def 1;

      end;

      reconsider R as RestFunc of S, T by A5, Def5;

      

       A13: (the carrier of S --> ( 0. T)) = L by LOPBAN_1: 31;

       A14:

      now

        let x0 be Point of S;

        assume

         A15: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A16: N c= Z by A1, Th2;

        

         A17: N c= ( dom f) by A2, A16;

        for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

        proof

          let x be Point of S;

          

           A18: (R /. (x - x0)) = (R . (x - x0)) by A4, PARTFUN1:def 6

          .= ( 0. T);

          assume x in N;

          

          hence ((f /. x) - (f /. x0)) = (r - (f /. x0)) by A11, A17

          .= (r - r) by A2, A11, A15

          .= ( 0. T) by RLVECT_1: 15

          .= (( 0. T) + ( 0. T)) by RLVECT_1: 4

          .= ((L . (x - x0)) + (R /. (x - x0))) by A13, A18;

        end;

        hence f is_differentiable_in x0 by A17;

      end;

      hence

       A19: f is_differentiable_on Z by A1, A2, Th31;

      let x0 be Point of S;

      assume

       A20: x0 in Z;

      then

       A21: f is_differentiable_in x0 by A14;

      then ex N be Neighbourhood of x0 st N c= ( dom f) & ex L, R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

      then

      consider N be Neighbourhood of x0 such that

       A22: N c= ( dom f);

      

       A23: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

      proof

        let x be Point of S;

        

         A24: (R /. (x - x0)) = (R . (x - x0)) by A4, PARTFUN1:def 6

        .= ( 0. T);

        assume x in N;

        

        hence ((f /. x) - (f /. x0)) = (r - (f /. x0)) by A11, A22

        .= (r - r) by A2, A11, A20

        .= ( 0. T) by RLVECT_1: 15

        .= (( 0. T) + ( 0. T)) by RLVECT_1: 4

        .= ((L . (x - x0)) + (R /. (x - x0))) by A13, A24;

      end;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A19, A20, Def9

      .= ( 0. ( R_NormSpace_of_BoundedLinearOperators (S,T))) by A21, A22, A23, Def7;

    end;

    registration

      let S;

      let h, n;

      cluster (h ^\ n) -> ( 0. S) -convergent;

      coherence

      proof

        

         A1: h is convergent by Def4;

        ( lim h) = ( 0. S) by Def4;

        then

         A2: ( lim (h ^\ n)) = ( 0. S) by A1, LOPBAN_3: 9;

        (h ^\ n) is convergent by A1, LOPBAN_3: 9;

        hence thesis by A2;

      end;

    end

    registration

      let S be non trivial RealNormSpace;

      let h be ( 0. S) -convergent non-zero sequence of S;

      let n;

      cluster (h ^\ n) -> ( 0. S) -convergent non-zero;

      coherence by Th17;

    end

    theorem :: NDIFF_1:34

    

     Th34: for x0 be Point of S holds for N be Neighbourhood of x0 st f is_differentiable_in x0 & N c= ( dom f) holds for h be ( 0. S) -convergent sequence of S st h is non-zero holds for c st ( rng c) = {x0} & ( rng (h + c)) c= N holds ((f /* (h + c)) - (f /* c)) is convergent & ( lim ((f /* (h + c)) - (f /* c))) = ( 0. T)

    proof

      let x0 be Point of S;

      let N be Neighbourhood of x0;

      assume that

       A1: f is_differentiable_in x0 and

       A2: N c= ( dom f);

      let h be ( 0. S) -convergent sequence of S;

      assume

       A3: h is non-zero;

      let c such that

       A4: ( rng c) = {x0} and

       A5: ( rng (h + c)) c= N;

      consider N1 be Neighbourhood of x0 such that N1 c= ( dom f) and

       A6: ex L, R st for x be Point of S st x in N1 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A1;

      consider N2 be Neighbourhood of x0 such that

       A7: N2 c= N and

       A8: N2 c= N1 by Th1;

      consider L, R such that

       A9: for x be Point of S st x in N1 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A6;

      consider g be Real such that

       A10: 0 < g and

       A11: { y where y be Point of S : ||.(y - x0).|| < g } c= N2 by NFCONT_1:def 1;

      

       A12: x0 in N2 by NFCONT_1: 4;

      ex n st ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2

      proof

        (c . 0 ) in ( rng c) by NFCONT_1: 6;

        then (c . 0 ) = x0 by A4, TARSKI:def 1;

        then

         A13: ( lim c) = x0 by Th18;

        

         A14: c is convergent & h is convergent by Def4, Th18;

        then

         A15: (h + c) is convergent by NORMSP_1: 19;

        ( lim h) = ( 0. S) by Def4;

        

        then ( lim (h + c)) = (( 0. S) + x0) by A13, A14, NORMSP_1: 25

        .= x0 by RLVECT_1: 4;

        then

        consider n be Nat such that

         A16: for m be Nat st n <= m holds ||.(((h + c) . m) - x0).|| < g by A10, A15, NORMSP_1:def 7;

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

        take n;

        

         A17: ( rng (c ^\ n)) = {x0} by A4, VALUED_0: 26;

        thus ( rng (c ^\ n)) c= N2 by A12, A17, TARSKI:def 1;

        let y be object;

        assume y in ( rng ((h + c) ^\ n));

        then

        consider m be Nat such that

         A18: y = (((h + c) ^\ n) . m) by NFCONT_1: 6;

        reconsider y1 = y as Point of S by A18;

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

        then ||.(((h + c) . (n + m)) - x0).|| < g by A16;

        then ||.((((h + c) ^\ n) . m) - x0).|| < g by NAT_1:def 3;

        then y1 in { z where z be Point of S : ||.(z - x0).|| < g } by A18;

        hence thesis by A11;

      end;

      then

      consider n such that ( rng (c ^\ n)) c= N2 and

       A19: ( rng ((h + c) ^\ n)) c= N2;

      

       A20: ( lim (h ^\ n)) = ( 0. S) by Def4;

      

       A21: for k holds ((f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k))) = ((L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)))

      proof

        let k;

        (((h + c) ^\ n) . k) in ( rng ((h + c) ^\ n)) by NFCONT_1: 6;

        then

         A22: (((h + c) ^\ n) . k) in N2 by A19;

        ((c ^\ n) . k) in ( rng (c ^\ n)) & ( rng (c ^\ n)) = ( rng c) by NFCONT_1: 6, VALUED_0: 26;

        then

         A23: ((c ^\ n) . k) = x0 by A4, TARSKI:def 1;

        ((((h + c) ^\ n) . k) - ((c ^\ n) . k)) = (((h + c) . (k + n)) - ((c ^\ n) . k)) by NAT_1:def 3

        .= (((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k)) by NORMSP_1:def 2

        .= ((((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k)) by NAT_1:def 3

        .= ((((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k)) by NAT_1:def 3

        .= (((h ^\ n) . k) + (((c ^\ n) . k) - ((c ^\ n) . k))) by RLVECT_1:def 3

        .= (((h ^\ n) . k) + ( 0. S)) by RLVECT_1: 15

        .= ((h ^\ n) . k) by RLVECT_1: 4;

        hence thesis by A9, A8, A22, A23;

      end;

      ( R_NormSpace_of_BoundedLinearOperators (S,T)) = NORMSTR (# ( BoundedLinearOperators (S,T)), ( Zero_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Add_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Mult_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;

      then

      reconsider L as Element of ( BoundedLinearOperators (S,T));

      reconsider LP = ( modetrans (L,S,T)) as PartFunc of S, T;

      

       A24: (h ^\ n) is non-zero by A3, Th17;

      then

       A25: ( lim (R /* (h ^\ n))) = ( 0. T) by Th24;

      

       A26: ( rng ((h + c) ^\ n)) c= ( dom f) by A19, A7, A2;

      R is total by Def5;

      then ( dom R) = the carrier of S by PARTFUN1:def 2;

      then

       A27: ( rng (h ^\ n)) c= ( dom R);

      

       A28: ( rng (c ^\ n)) c= ( dom f)

      proof

        let y be object;

        assume

         A29: y in ( rng (c ^\ n));

        ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        then y = x0 by A4, A29, TARSKI:def 1;

        then y in N by NFCONT_1: 4;

        hence thesis by A2;

      end;

      

       A30: ( dom ( modetrans (L,S,T))) = the carrier of S by FUNCT_2:def 1;

      then

       A31: ( rng (h ^\ n)) c= ( dom ( modetrans (L,S,T)));

      now

        let k;

        

        thus (((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k) = (((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k)) by NORMSP_1:def 3

        .= ((f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k)) by A26, FUNCT_2: 109

        .= ((f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k))) by A28, FUNCT_2: 109

        .= ((L . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))) by A21

        .= ((( modetrans (L,S,T)) . ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))) by LOPBAN_1:def 11

        .= ((LP /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))) by A30, PARTFUN1:def 6

        .= (((LP /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k))) by A31, FUNCT_2: 109

        .= (((LP /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k)) by A27, FUNCT_2: 109

        .= (((LP /* (h ^\ n)) + (R /* (h ^\ n))) . k) by NORMSP_1:def 2;

      end;

      then

       A32: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) = ((LP /* (h ^\ n)) + (R /* (h ^\ n))) by FUNCT_2: 63;

      

       A33: ( dom ( modetrans (L,S,T))) = the carrier of S by FUNCT_2:def 1;

      LP is_Lipschitzian_on the carrier of S

      proof

        thus the carrier of S c= ( dom LP) by FUNCT_2:def 1;

        set LL = ( modetrans (L,S,T));

        consider K be Real such that

         A34: 0 <= K and

         A35: for x be VECTOR of S holds ||.(LL . x).|| <= (K * ||.x.||) by LOPBAN_1:def 8;

        take (K + 1);

        

         A36: ( 0 + K) < (1 + K) by XREAL_1: 8;

        now

          let x1,x2 be Point of S such that x1 in the carrier of S and x2 in the carrier of S;

          

           A37: ||.(LL . (x1 - x2)).|| <= (K * ||.(x1 - x2).||) by A35;

           0 <= ||.(x1 - x2).|| by NORMSP_1: 4;

          then

           A38: (K * ||.(x1 - x2).||) <= ((K + 1) * ||.(x1 - x2).||) by A36, XREAL_1: 64;

           ||.((LP /. x1) - (LP /. x2)).|| = ||.((LL . x1) - (LP /. x2)).|| by A33, PARTFUN1:def 6

          .= ||.((LL . x1) + ( - (LL . x2))).|| by A33, PARTFUN1:def 6

          .= ||.((LL . x1) + (( - 1) * (LL . x2))).|| by RLVECT_1: 16

          .= ||.((LL . x1) + (LL . (( - 1) * x2))).|| by LOPBAN_1:def 5

          .= ||.(LL . (x1 + (( - 1) * x2))).|| by VECTSP_1:def 20

          .= ||.(LL . (x1 - x2)).|| by RLVECT_1: 16;

          hence ||.((LP /. x1) - (LP /. x2)).|| <= ((K + 1) * ||.(x1 - x2).||) by A37, A38, XXREAL_0: 2;

        end;

        hence thesis by A34;

      end;

      then

       A39: LP is_continuous_on the carrier of S by NFCONT_1: 45;

      

       A40: ( rng c) c= ( dom f)

      proof

        let y be object;

        assume y in ( rng c);

        then y = x0 by A4, TARSKI:def 1;

        then y in N by NFCONT_1: 4;

        hence thesis by A2;

      end;

      

       A41: (h ^\ n) is convergent & ( rng (h ^\ n)) c= the carrier of S by Def4;

      then

       A42: (LP /* (h ^\ n)) is convergent by A39, A20, NFCONT_1: 18;

      

       A43: (R /* (h ^\ n)) is convergent by A24, Th24;

      then

       A44: ((LP /* (h ^\ n)) + (R /* (h ^\ n))) is convergent by A42, NORMSP_1: 19;

      (LP /. ( 0. S)) = (( modetrans (L,S,T)) . ( 0. S)) by A33, PARTFUN1:def 6

      .= (( modetrans (L,S,T)) . ( 0 * ( 0. S))) by RLVECT_1: 10

      .= ( 0 * (( modetrans (L,S,T)) . ( 0. S))) by LOPBAN_1:def 5

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

      then ( lim (LP /* (h ^\ n))) = ( 0. T) by A39, A41, A20, NFCONT_1: 18;

      then ( lim ((LP /* (h ^\ n)) + (R /* (h ^\ n)))) = (( 0. T) + ( 0. T)) by A43, A25, A42, NORMSP_1: 25;

      then

       A45: ( lim ((LP /* (h ^\ n)) + (R /* (h ^\ n)))) = ( 0. T) by RLVECT_1: 4;

      ( rng (h + c)) c= ( dom f) by A5, A2;

      

      then ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) = (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) by VALUED_0: 27

      .= (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) by A40, VALUED_0: 27

      .= (((f /* (h + c)) - (f /* c)) ^\ n) by Th16;

      hence thesis by A32, A44, A45, LOPBAN_3: 10, LOPBAN_3: 11;

    end;

    theorem :: NDIFF_1:35

    

     Th35: for f1, f2, x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds (f1 + f2) is_differentiable_in x0 & ( diff ((f1 + f2),x0)) = (( diff (f1,x0)) + ( diff (f2,x0)))

    proof

      let f1, f2, x0;

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A3: N1 c= ( dom f1) and

       A4: ex L, R st for x be Point of S st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A1;

      consider L1, R1 such that

       A5: for x be Point of S st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L1 . (x - x0)) + (R1 /. (x - x0))) by A4;

      consider N2 be Neighbourhood of x0 such that

       A6: N2 c= ( dom f2) and

       A7: ex L, R st for x be Point of S st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A2;

      consider L2, R2 such that

       A8: for x be Point of S st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L2 . (x - x0)) + (R2 /. (x - x0))) by A7;

      reconsider R = (R1 + R2) as RestFunc of S, T by Th28;

      set L = (L1 + L2);

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 and

       A10: N c= N2 by Th1;

      

       A11: N c= ( dom f2) by A6, A10;

      N c= ( dom f1) by A3, A9;

      then (N /\ N) c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 27;

      then

       A12: N c= ( dom (f1 + f2)) by VFUNCT_1:def 1;

      

       A13: R1 is total & R2 is total by Def5;

       A14:

      now

        let x be Point of S;

        

         A15: x0 in N by NFCONT_1: 4;

        assume

         A16: x in N;

        

        hence (((f1 + f2) /. x) - ((f1 + f2) /. x0)) = (((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0)) by A12, VFUNCT_1:def 1

        .= (((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0))) by A12, A15, VFUNCT_1:def 1

        .= ((((f1 /. x) + (f2 /. x)) - (f1 /. x0)) - (f2 /. x0)) by RLVECT_1: 27

        .= ((((f1 /. x) + ( - (f1 /. x0))) + (f2 /. x)) - (f2 /. x0)) by RLVECT_1:def 3

        .= (((f1 /. x) - (f1 /. x0)) + ((f2 /. x) - (f2 /. x0))) by RLVECT_1:def 3

        .= (((L1 . (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0))) by A5, A9, A16

        .= (((L1 . (x - x0)) + (R1 /. (x - x0))) + ((L2 . (x - x0)) + (R2 /. (x - x0)))) by A8, A10, A16

        .= ((((R1 /. (x - x0)) + (L1 . (x - x0))) + (L2 . (x - x0))) + (R2 /. (x - x0))) by RLVECT_1:def 3

        .= ((((L1 . (x - x0)) + (L2 . (x - x0))) + (R1 /. (x - x0))) + (R2 /. (x - x0))) by RLVECT_1:def 3

        .= (((L1 . (x - x0)) + (L2 . (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0)))) by RLVECT_1:def 3

        .= ((L . (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0)))) by LOPBAN_1: 35

        .= ((L . (x - x0)) + (R /. (x - x0))) by A13, VFUNCT_1: 37;

      end;

      hence (f1 + f2) is_differentiable_in x0 by A12;

      

      hence ( diff ((f1 + f2),x0)) = L by A12, A14, Def7

      .= (( diff (f1,x0)) + L2) by A1, A3, A5, Def7

      .= (( diff (f1,x0)) + ( diff (f2,x0))) by A2, A6, A8, Def7;

    end;

    theorem :: NDIFF_1:36

    

     Th36: for f1, f2, x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds (f1 - f2) is_differentiable_in x0 & ( diff ((f1 - f2),x0)) = (( diff (f1,x0)) - ( diff (f2,x0)))

    proof

      let f1, f2, x0;

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A3: N1 c= ( dom f1) and

       A4: ex L, R st for x be Point of S st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A1;

      consider L1, R1 such that

       A5: for x be Point of S st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L1 . (x - x0)) + (R1 /. (x - x0))) by A4;

      consider N2 be Neighbourhood of x0 such that

       A6: N2 c= ( dom f2) and

       A7: ex L, R st for x be Point of S st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A2;

      consider L2, R2 such that

       A8: for x be Point of S st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L2 . (x - x0)) + (R2 /. (x - x0))) by A7;

      reconsider R = (R1 - R2) as RestFunc of S, T by Th28;

      set L = (L1 - L2);

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 and

       A10: N c= N2 by Th1;

      

       A11: N c= ( dom f2) by A6, A10;

      N c= ( dom f1) by A3, A9;

      then (N /\ N) c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 27;

      then

       A12: N c= ( dom (f1 - f2)) by VFUNCT_1:def 2;

      

       A13: R1 is total & R2 is total by Def5;

       A14:

      now

        let x be Point of S;

        

         A15: x0 in N by NFCONT_1: 4;

        assume

         A16: x in N;

        

        hence (((f1 - f2) /. x) - ((f1 - f2) /. x0)) = (((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0)) by A12, VFUNCT_1:def 2

        .= (((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0))) by A12, A15, VFUNCT_1:def 2

        .= ((((f1 /. x) - (f2 /. x)) - (f1 /. x0)) + (f2 /. x0)) by RLVECT_1: 29

        .= (((f1 /. x) - ((f1 /. x0) + (f2 /. x))) + (f2 /. x0)) by RLVECT_1: 27

        .= ((((f1 /. x) - (f1 /. x0)) - (f2 /. x)) + (f2 /. x0)) by RLVECT_1: 27

        .= (((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0))) by RLVECT_1: 29

        .= (((L1 . (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0))) by A5, A9, A16

        .= (((L1 . (x - x0)) + (R1 /. (x - x0))) - ((L2 . (x - x0)) + (R2 /. (x - x0)))) by A8, A10, A16

        .= ((((L1 . (x - x0)) + (R1 /. (x - x0))) - (L2 . (x - x0))) - (R2 /. (x - x0))) by RLVECT_1: 27

        .= (((L1 . (x - x0)) + ((R1 /. (x - x0)) + ( - (L2 . (x - x0))))) - (R2 /. (x - x0))) by RLVECT_1:def 3

        .= (((L1 . (x - x0)) - ((L2 . (x - x0)) - (R1 /. (x - x0)))) - (R2 /. (x - x0))) by RLVECT_1: 33

        .= ((((L1 . (x - x0)) - (L2 . (x - x0))) + (R1 /. (x - x0))) - (R2 /. (x - x0))) by RLVECT_1: 29

        .= (((L1 . (x - x0)) - (L2 . (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) by RLVECT_1:def 3

        .= ((L . (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) by LOPBAN_1: 40

        .= ((L . (x - x0)) + (R /. (x - x0))) by A13, VFUNCT_1: 37;

      end;

      hence (f1 - f2) is_differentiable_in x0 by A12;

      

      hence ( diff ((f1 - f2),x0)) = L by A12, A14, Def7

      .= (( diff (f1,x0)) - L2) by A1, A3, A5, Def7

      .= (( diff (f1,x0)) - ( diff (f2,x0))) by A2, A6, A8, Def7;

    end;

    theorem :: NDIFF_1:37

    

     Th37: for r, f, x0 st f is_differentiable_in x0 holds (r (#) f) is_differentiable_in x0 & ( diff ((r (#) f),x0)) = (r * ( diff (f,x0)))

    proof

      let r, f, x0;

      assume

       A1: f is_differentiable_in x0;

      then

      consider N1 be Neighbourhood of x0 such that

       A2: N1 c= ( dom f) and

       A3: ex L, R st for x be Point of S st x in N1 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

      consider L1, R1 such that

       A4: for x be Point of S st x in N1 holds ((f /. x) - (f /. x0)) = ((L1 . (x - x0)) + (R1 /. (x - x0))) by A3;

      reconsider R = (r (#) R1) as RestFunc of S, T by Th29;

      set L = (r * L1);

      

       A5: N1 c= ( dom (r (#) f)) by A2, VFUNCT_1:def 4;

      

       A6: R1 is total by Def5;

       A7:

      now

        let x be Point of S;

        

         A8: x0 in N1 by NFCONT_1: 4;

        assume

         A9: x in N1;

        

        hence (((r (#) f) /. x) - ((r (#) f) /. x0)) = ((r * (f /. x)) - ((r (#) f) /. x0)) by A5, VFUNCT_1:def 4

        .= ((r * (f /. x)) - (r * (f /. x0))) by A5, A8, VFUNCT_1:def 4

        .= (r * ((f /. x) - (f /. x0))) by RLVECT_1: 34

        .= (r * ((L1 . (x - x0)) + (R1 /. (x - x0)))) by A4, A9

        .= ((r * (L1 . (x - x0))) + (r * (R1 /. (x - x0)))) by RLVECT_1:def 5

        .= ((L . (x - x0)) + (r * (R1 /. (x - x0)))) by LOPBAN_1: 36

        .= ((L . (x - x0)) + (R /. (x - x0))) by A6, VFUNCT_1: 39;

      end;

      hence (r (#) f) is_differentiable_in x0 by A5;

      

      hence ( diff ((r (#) f),x0)) = L by A5, A7, Def7

      .= (r * ( diff (f,x0))) by A1, A2, A4, Def7;

    end;

    theorem :: NDIFF_1:38

    for f be PartFunc of S, S holds for Z be Subset of S st Z is open & Z c= ( dom f) & (f | Z) = ( id Z) holds f is_differentiable_on Z & for x be Point of S st x in Z holds ((f `| Z) /. x) = ( id the carrier of S)

    proof

      set L = ( id the carrier of S);

      ( R_NormSpace_of_BoundedLinearOperators (S,S)) = NORMSTR (# ( BoundedLinearOperators (S,S)), ( Zero_ (( BoundedLinearOperators (S,S)),( R_VectorSpace_of_LinearOperators (S,S)))), ( Add_ (( BoundedLinearOperators (S,S)),( R_VectorSpace_of_LinearOperators (S,S)))), ( Mult_ (( BoundedLinearOperators (S,S)),( R_VectorSpace_of_LinearOperators (S,S)))), ( BoundedLinearOperatorsNorm (S,S)) #) & L is Lipschitzian LinearOperator of S, S by LOPBAN_1:def 14, LOPBAN_2: 3;

      then

      reconsider L as Point of ( R_NormSpace_of_BoundedLinearOperators (S,S)) by LOPBAN_1:def 9;

      let f be PartFunc of S, S;

      let Z be Subset of S such that

       A1: Z is open;

      reconsider R = (the carrier of S --> ( 0. S)) as PartFunc of S, S;

      

       A2: ( dom R) = the carrier of S;

      now

        let h;

        assume h is non-zero;

         A3:

        now

          let n be Nat;

          

           A4: (R /. (h . n)) = (R . (h . n)) by A2, PARTFUN1:def 6

          .= ( 0. S);

          

           A5: ( rng h) c= ( dom R);

          

           A6: n in NAT by ORDINAL1:def 12;

          

          thus ((( ||.h.|| " ) (#) (R /* h)) . n) = ((( ||.h.|| " ) . n) * ((R /* h) . n)) by Def2

          .= ((( ||.h.|| " ) . n) * (R /. (h . n))) by A6, A5, FUNCT_2: 109

          .= ( 0. S) by A4, RLVECT_1: 10;

        end;

        then

         A7: (( ||.h.|| " ) (#) (R /* h)) is constant by VALUED_0:def 18;

        hence (( ||.h.|| " ) (#) (R /* h)) is convergent by Th18;

        ((( ||.h.|| " ) (#) (R /* h)) . 0 ) = ( 0. S) by A3;

        hence ( lim (( ||.h.|| " ) (#) (R /* h))) = ( 0. S) by A7, Th18;

      end;

      then

      reconsider R as RestFunc of S, S by Def5;

      assume that

       A8: Z c= ( dom f) and

       A9: (f | Z) = ( id Z);

       A10:

      now

        let x be Point of S;

        assume

         A11: x in Z;

        then ((f | Z) . x) = x by A9, FUNCT_1: 18;

        then (f . x) = x by A11, FUNCT_1: 49;

        hence (f /. x) = x by A8, A11, PARTFUN1:def 6;

      end;

       A12:

      now

        let x0 be Point of S;

        assume

         A13: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A14: N c= Z by A1, Th2;

        

         A15: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

        proof

          let x be Point of S;

          

           A16: (R /. (x - x0)) = (R . (x - x0)) by A2, PARTFUN1:def 6

          .= ( 0. S);

          assume x in N;

          

          hence ((f /. x) - (f /. x0)) = (x - (f /. x0)) by A10, A14

          .= (x - x0) by A10, A13

          .= (L . (x - x0))

          .= ((L . (x - x0)) + (R /. (x - x0))) by A16, RLVECT_1: 4;

        end;

        N c= ( dom f) by A8, A14;

        hence f is_differentiable_in x0 by A15;

      end;

      hence

       A17: f is_differentiable_on Z by A1, A8, Th31;

      let x0 be Point of S;

      assume

       A18: x0 in Z;

      then

      consider N1 be Neighbourhood of x0 such that

       A19: N1 c= Z by A1, Th2;

      

       A20: f is_differentiable_in x0 by A12, A18;

      then ex N be Neighbourhood of x0 st N c= ( dom f) & ex L be Point of ( R_NormSpace_of_BoundedLinearOperators (S,S)), R be RestFunc of S, S st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

      then

      consider N be Neighbourhood of x0 such that

       A21: N c= ( dom f);

      consider N2 be Neighbourhood of x0 such that

       A22: N2 c= N1 and

       A23: N2 c= N by Th1;

      

       A24: N2 c= ( dom f) by A21, A23;

      

       A25: for x be Point of S st x in N2 holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

      proof

        let x be Point of S;

        

         A26: (R /. (x - x0)) = (R . (x - x0)) by A2, PARTFUN1:def 6

        .= ( 0. S);

        assume x in N2;

        then x in N1 by A22;

        

        hence ((f /. x) - (f /. x0)) = (x - (f /. x0)) by A10, A19

        .= (x - x0) by A10, A18

        .= (L . (x - x0))

        .= ((L . (x - x0)) + (R /. (x - x0))) by A26, RLVECT_1: 4;

      end;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A17, A18, Def9

      .= ( id the carrier of S) by A20, A24, A25, Def7;

    end;

    theorem :: NDIFF_1:39

    for Z be Subset of S st Z is open holds for f1, f2 st Z c= ( dom (f1 + f2)) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds (f1 + f2) is_differentiable_on Z & for x be Point of S st x in Z holds (((f1 + f2) `| Z) /. x) = (( diff (f1,x)) + ( diff (f2,x)))

    proof

      let Z be Subset of S such that

       A1: Z is open;

      let f1, f2;

      assume that

       A2: Z c= ( dom (f1 + f2)) and

       A3: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0 be Point of S;

        assume x0 in Z;

        then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1, A3, Th31;

        hence (f1 + f2) is_differentiable_in x0 by Th35;

      end;

      hence

       A4: (f1 + f2) is_differentiable_on Z by A1, A2, Th31;

      now

        let x be Point of S;

        assume

         A5: x in Z;

        then

         A6: f1 is_differentiable_in x & f2 is_differentiable_in x by A1, A3, Th31;

        

        thus (((f1 + f2) `| Z) /. x) = ( diff ((f1 + f2),x)) by A4, A5, Def9

        .= (( diff (f1,x)) + ( diff (f2,x))) by A6, Th35;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_1:40

    for Z be Subset of S st Z is open holds for f1, f2 st Z c= ( dom (f1 - f2)) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds (f1 - f2) is_differentiable_on Z & for x be Point of S st x in Z holds (((f1 - f2) `| Z) /. x) = (( diff (f1,x)) - ( diff (f2,x)))

    proof

      let Z be Subset of S such that

       A1: Z is open;

      let f1, f2;

      assume that

       A2: Z c= ( dom (f1 - f2)) and

       A3: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0 be Point of S;

        assume x0 in Z;

        then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1, A3, Th31;

        hence (f1 - f2) is_differentiable_in x0 by Th36;

      end;

      hence

       A4: (f1 - f2) is_differentiable_on Z by A1, A2, Th31;

      now

        let x be Point of S;

        assume

         A5: x in Z;

        then

         A6: f1 is_differentiable_in x & f2 is_differentiable_in x by A1, A3, Th31;

        

        thus (((f1 - f2) `| Z) /. x) = ( diff ((f1 - f2),x)) by A4, A5, Def9

        .= (( diff (f1,x)) - ( diff (f2,x))) by A6, Th36;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_1:41

    for Z be Subset of S st Z is open holds for r, f st Z c= ( dom (r (#) f)) & f is_differentiable_on Z holds (r (#) f) is_differentiable_on Z & for x be Point of S st x in Z holds (((r (#) f) `| Z) /. x) = (r * ( diff (f,x)))

    proof

      let Z be Subset of S such that

       A1: Z is open;

      let r, f;

      assume that

       A2: Z c= ( dom (r (#) f)) and

       A3: f is_differentiable_on Z;

      now

        let x0 be Point of S;

        assume x0 in Z;

        then f is_differentiable_in x0 by A1, A3, Th31;

        hence (r (#) f) is_differentiable_in x0 by Th37;

      end;

      hence

       A4: (r (#) f) is_differentiable_on Z by A1, A2, Th31;

      now

        let x be Point of S;

        assume

         A5: x in Z;

        then

         A6: f is_differentiable_in x by A1, A3, Th31;

        

        thus (((r (#) f) `| Z) /. x) = ( diff ((r (#) f),x)) by A4, A5, Def9

        .= (r * ( diff (f,x))) by A6, Th37;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_1:42

    for Z be Subset of S st Z is open holds (Z c= ( dom f) & (f | Z) is constant implies f is_differentiable_on Z & for x be Point of S st x in Z holds ((f `| Z) /. x) = ( 0. ( R_NormSpace_of_BoundedLinearOperators (S,T))))

    proof

      let Z be Subset of S such that

       A1: Z is open;

      reconsider R = (the carrier of S --> ( 0. T)) as PartFunc of S, T;

      set L = ( 0. ( R_NormSpace_of_BoundedLinearOperators (S,T)));

      assume that

       A2: Z c= ( dom f) and

       A3: (f | Z) is constant;

      ( R_NormSpace_of_BoundedLinearOperators (S,T)) = NORMSTR (# ( BoundedLinearOperators (S,T)), ( Zero_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Add_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Mult_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;

      then

      reconsider L as Element of ( BoundedLinearOperators (S,T));

      

       A4: ( dom R) = the carrier of S;

      now

        let h;

        assume h is non-zero;

         A5:

        now

          let n be Nat;

          

           A6: (R /. (h . n)) = (R . (h . n)) by A4, PARTFUN1:def 6

          .= ( 0. T);

          

           A7: ( rng h) c= ( dom R);

          

           A8: n in NAT by ORDINAL1:def 12;

          

          thus ((( ||.h.|| " ) (#) (R /* h)) . n) = ((( ||.h.|| " ) . n) * ((R /* h) . n)) by Def2

          .= ((( ||.h.|| " ) . n) * (R /. (h . n))) by A8, A7, FUNCT_2: 109

          .= ( 0. T) by A6, RLVECT_1: 10;

        end;

        then

         A9: (( ||.h.|| " ) (#) (R /* h)) is constant by VALUED_0:def 18;

        hence (( ||.h.|| " ) (#) (R /* h)) is convergent by Th18;

        ((( ||.h.|| " ) (#) (R /* h)) . 0 ) = ( 0. T) by A5;

        hence ( lim (( ||.h.|| " ) (#) (R /* h))) = ( 0. T) by A9, Th18;

      end;

      then

      reconsider R as RestFunc of S, T by Def5;

      consider r be Point of T such that

       A10: for x be Point of S st x in (Z /\ ( dom f)) holds (f . x) = r by A3, PARTFUN2: 57;

       A11:

      now

        let x be Point of S;

        assume

         A12: x in (Z /\ ( dom f));

        (Z /\ ( dom f)) c= ( dom f) by XBOOLE_1: 17;

        

        hence (f /. x) = (f . x) by A12, PARTFUN1:def 6

        .= r by A10, A12;

      end;

      

       A13: (the carrier of S --> ( 0. T)) = L by LOPBAN_1: 31;

       A14:

      now

        let x0 be Point of S;

        assume

         A15: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A16: N c= Z by A1, Th2;

        

         A17: N c= ( dom f) by A2, A16;

        

         A18: x0 in (Z /\ ( dom f)) by A2, A15, XBOOLE_0:def 4;

        for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

        proof

          let x be Point of S;

          

           A19: (R /. (x - x0)) = (R . (x - x0)) by A4, PARTFUN1:def 6

          .= ( 0. T);

          assume x in N;

          then x in (Z /\ ( dom f)) by A16, A17, XBOOLE_0:def 4;

          

          hence ((f /. x) - (f /. x0)) = (r - (f /. x0)) by A11

          .= (r - r) by A11, A18

          .= ( 0. T) by RLVECT_1: 15

          .= (( 0. T) + ( 0. T)) by RLVECT_1: 4

          .= ((L . (x - x0)) + (R /. (x - x0))) by A13, A19;

        end;

        hence f is_differentiable_in x0 by A17;

      end;

      hence

       A20: f is_differentiable_on Z by A1, A2, Th31;

      let x0 be Point of S;

      assume

       A21: x0 in Z;

      then

      consider N be Neighbourhood of x0 such that

       A22: N c= Z by A1, Th2;

      

       A23: N c= ( dom f) by A2, A22;

      

       A24: x0 in (Z /\ ( dom f)) by A2, A21, XBOOLE_0:def 4;

      

       A25: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

      proof

        let x be Point of S;

        

         A26: (R /. (x - x0)) = (R . (x - x0)) by A4, PARTFUN1:def 6

        .= ( 0. T);

        assume x in N;

        then x in (Z /\ ( dom f)) by A22, A23, XBOOLE_0:def 4;

        

        hence ((f /. x) - (f /. x0)) = (r - (f /. x0)) by A11

        .= (r - r) by A11, A24

        .= ( 0. T) by RLVECT_1: 15

        .= (( 0. T) + ( 0. T)) by RLVECT_1: 4

        .= ((L . (x - x0)) + (R /. (x - x0))) by A13, A26;

      end;

      

       A27: f is_differentiable_in x0 by A14, A21;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A20, A21, Def9

      .= ( 0. ( R_NormSpace_of_BoundedLinearOperators (S,T))) by A27, A23, A25, Def7;

    end;

    theorem :: NDIFF_1:43

    for f be PartFunc of S, S holds for r be Real holds for p be Point of S holds for Z be Subset of S st Z is open holds (Z c= ( dom f) & (for x be Point of S st x in Z holds (f /. x) = ((r * x) + p)) implies f is_differentiable_on Z & for x be Point of S st x in Z holds ((f `| Z) /. x) = (r * ( FuncUnit S)))

    proof

      let f be PartFunc of S, S;

      let r be Real;

      let p be Point of S;

      let Z be Subset of S such that

       A1: Z is open;

      

       A2: ( R_NormSpace_of_BoundedLinearOperators (S,S)) = NORMSTR (# ( BoundedLinearOperators (S,S)), ( Zero_ (( BoundedLinearOperators (S,S)),( R_VectorSpace_of_LinearOperators (S,S)))), ( Add_ (( BoundedLinearOperators (S,S)),( R_VectorSpace_of_LinearOperators (S,S)))), ( Mult_ (( BoundedLinearOperators (S,S)),( R_VectorSpace_of_LinearOperators (S,S)))), ( BoundedLinearOperatorsNorm (S,S)) #) by LOPBAN_1:def 14;

      then

      reconsider II = ( FuncUnit S) as Point of ( R_NormSpace_of_BoundedLinearOperators (S,S));

      set L = (r * II);

      reconsider L as Point of ( R_NormSpace_of_BoundedLinearOperators (S,S));

      reconsider R = (the carrier of S --> ( 0. S)) as PartFunc of S, S;

      assume that

       A3: Z c= ( dom f) and

       A4: for x be Point of S st x in Z holds (f /. x) = ((r * x) + p);

      

       A5: L = (r * ( FuncUnit S)) by A2, LOPBAN_2:def 3;

      

       A6: ( dom R) = the carrier of S;

      now

        let h;

        assume h is non-zero;

         A7:

        now

          let n be Nat;

          

           A8: (R /. (h . n)) = (R . (h . n)) by A6, PARTFUN1:def 6

          .= ( 0. S);

          

           A9: ( rng h) c= ( dom R);

          

           A10: n in NAT by ORDINAL1:def 12;

          

          thus ((( ||.h.|| " ) (#) (R /* h)) . n) = ((( ||.h.|| " ) . n) * ((R /* h) . n)) by Def2

          .= ((( ||.h.|| " ) . n) * (R /. (h . n))) by A10, A9, FUNCT_2: 109

          .= ( 0. S) by A8, RLVECT_1: 10;

        end;

        then

         A11: (( ||.h.|| " ) (#) (R /* h)) is constant by VALUED_0:def 18;

        hence (( ||.h.|| " ) (#) (R /* h)) is convergent by Th18;

        ((( ||.h.|| " ) (#) (R /* h)) . 0 ) = ( 0. S) by A7;

        hence ( lim (( ||.h.|| " ) (#) (R /* h))) = ( 0. S) by A11, Th18;

      end;

      then

      reconsider R as RestFunc of S, S by Def5;

       A12:

      now

        let x0 be Point of S;

        assume

         A13: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A14: N c= Z by A1, Th2;

        

         A15: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

        proof

          let x be Point of S;

          

           A16: (R /. (x - x0)) = (R . (x - x0)) by A6, PARTFUN1:def 6

          .= ( 0. S);

          (x - x0) = (( id the carrier of S) . (x - x0));

          

          then

           A17: (r * (x - x0)) = (r * (( FuncUnit S) . (x - x0))) by LOPBAN_2:def 5

          .= (L . (x - x0)) by LOPBAN_1: 36;

          assume x in N;

          

          hence ((f /. x) - (f /. x0)) = (((r * x) + p) - (f /. x0)) by A4, A14

          .= (((r * x) + p) - ((r * x0) + p)) by A4, A13

          .= ((r * x) + (p - ((r * x0) + p))) by RLVECT_1:def 3

          .= ((r * x) + ((p - (r * x0)) - p)) by RLVECT_1: 27

          .= ((r * x) + ((p + ( - (r * x0))) - p))

          .= ((r * x) + (( - (r * x0)) + (p - p))) by RLVECT_1:def 3

          .= ((r * x) + (( - (r * x0)) + ( 0. S))) by RLVECT_1: 15

          .= ((r * x) - (r * x0)) by RLVECT_1: 4

          .= (r * (x - x0)) by RLVECT_1: 34

          .= ((L . (x - x0)) + (R /. (x - x0))) by A16, A17, RLVECT_1: 4;

        end;

        N c= ( dom f) by A3, A14;

        hence f is_differentiable_in x0 by A15;

      end;

      hence

       A18: f is_differentiable_on Z by A1, A3, Th31;

      let x0 be Point of S;

      assume

       A19: x0 in Z;

      then

      consider N be Neighbourhood of x0 such that

       A20: N c= Z by A1, Th2;

      

       A21: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)))

      proof

        let x be Point of S;

        

         A22: (R /. (x - x0)) = (R . (x - x0)) by A6, PARTFUN1:def 6

        .= ( 0. S);

        (x - x0) = (( id the carrier of S) . (x - x0));

        

        then

         A23: (r * (x - x0)) = (r * (( FuncUnit S) . (x - x0))) by LOPBAN_2:def 5

        .= (L . (x - x0)) by LOPBAN_1: 36;

        assume x in N;

        

        hence ((f /. x) - (f /. x0)) = (((r * x) + p) - (f /. x0)) by A4, A20

        .= (((r * x) + p) - ((r * x0) + p)) by A4, A19

        .= ((r * x) + (p - ((r * x0) + p))) by RLVECT_1:def 3

        .= ((r * x) + ((p - (r * x0)) - p)) by RLVECT_1: 27

        .= ((r * x) + ((p + ( - (r * x0))) - p))

        .= ((r * x) + (( - (r * x0)) + (p - p))) by RLVECT_1:def 3

        .= ((r * x) + (( - (r * x0)) + ( 0. S))) by RLVECT_1: 15

        .= ((r * x) - (r * x0)) by RLVECT_1: 4

        .= (r * (x - x0)) by RLVECT_1: 34

        .= ((L . (x - x0)) + (R /. (x - x0))) by A22, A23, RLVECT_1: 4;

      end;

      

       A24: N c= ( dom f) by A3, A20;

      

       A25: f is_differentiable_in x0 by A12, A19;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A18, A19, Def9

      .= (r * ( FuncUnit S)) by A5, A25, A24, A21, Def7;

    end;

    theorem :: NDIFF_1:44

    

     Th44: for x0 be Point of S holds f is_differentiable_in x0 implies f is_continuous_in x0

    proof

      let x0 be Point of S;

      assume

       A1: f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A2: N c= ( dom f) and ex L, R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

       A3:

      now

        consider g be Real such that

         A4: 0 < g and

         A5: { y where y be Point of S : ||.(y - x0).|| < g } c= N by NFCONT_1:def 1;

        reconsider s2 = ( NAT --> x0) as sequence of S;

        let s1 be sequence of S such that

         A6: ( rng s1) c= ( dom f) and

         A7: s1 is convergent and

         A8: ( lim s1) = x0 and

         A9: for n be Nat holds (s1 . n) <> x0;

        consider l be Nat such that

         A10: for m be Nat st l <= m holds ||.((s1 . m) - x0).|| < g by A7, A8, A4, NORMSP_1:def 7;

        deffunc G( Nat) = ((s1 . $1) - (s2 . $1));

        consider s3 be sequence of S such that

         A11: for n holds (s3 . n) = G(n) from FUNCT_2:sch 4;

        

         A12: for n be Nat holds (s3 . n) = G(n)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A11;

        end;

         A13:

        now

          given n such that

           A14: (s3 . n) = ( 0. S);

          ((s1 . n) - (s2 . n)) = ( 0. S) by A12, A14;

          then ((s1 . n) - x0) = ( 0. S);

          hence contradiction by A9, RLVECT_1: 21;

        end;

        now

          given n be Nat such that

           A15: ((s3 ^\ l) . n) = ( 0. S);

          

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

          (s3 . (n + l)) = ( 0. S) by A15, NAT_1:def 3;

          hence contradiction by A13, A16;

        end;

        then

         A17: (s3 ^\ l) is non-zero by Th7;

        reconsider c = (s2 ^\ l) as constant sequence of S;

        

         A18: s3 = (s1 - s2) by A12, NORMSP_1:def 3;

        

         A19: s2 is convergent by Th18;

        then

         A20: s3 is convergent by A7, A18, NORMSP_1: 20;

        then

         A21: (s3 ^\ l) is convergent by LOPBAN_3: 9;

        ( lim s2) = (s2 . 0 ) by Th18

        .= x0;

        

        then ( lim s3) = (x0 - x0) by A7, A8, A19, A18, NORMSP_1: 26

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

        then ( lim (s3 ^\ l)) = ( 0. S) by A20, LOPBAN_3: 9;

        then

        reconsider h = (s3 ^\ l) as ( 0. S) -convergent sequence of S by A21, Def4;

        now

          let n;

          

          thus ((((f /* (h + c)) - (f /* c)) + (f /* c)) . n) = ((((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n)) by NORMSP_1:def 2

          .= ((((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n)) by NORMSP_1:def 3

          .= (((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n))) by RLVECT_1: 29

          .= (((f /* (h + c)) . n) - ( 0. T)) by RLVECT_1: 15

          .= ((f /* (h + c)) . n) by RLVECT_1: 13;

        end;

        then

         A22: (((f /* (h + c)) - (f /* c)) + (f /* c)) = (f /* (h + c)) by FUNCT_2: 63;

        now

          let n;

          

          thus ((h + c) . n) = ((((s1 - s2) + s2) ^\ l) . n) by A18, Th15

          .= (((s1 - s2) + s2) . (n + l)) by NAT_1:def 3

          .= (((s1 - s2) . (n + l)) + (s2 . (n + l))) by NORMSP_1:def 2

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

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

          .= ((s1 . (n + l)) - ( 0. S)) by RLVECT_1: 15

          .= (s1 . (l + n)) by RLVECT_1: 13

          .= ((s1 ^\ l) . n) by NAT_1:def 3;

        end;

        

        then

         A23: (((f /* (h + c)) - (f /* c)) + (f /* c)) = (f /* (s1 ^\ l)) by A22, FUNCT_2: 63

        .= ((f /* s1) ^\ l) by A6, VALUED_0: 27;

        

         A24: ( rng c) = {x0}

        proof

          thus ( rng c) c= {x0}

          proof

            let y be object;

            assume y in ( rng c);

            then

            consider n be Nat such that

             A25: y = ((s2 ^\ l) . n) by NFCONT_1: 6;

            

             A26: (n + l) in NAT by ORDINAL1:def 12;

            y = (s2 . (n + l)) by A25, NAT_1:def 3;

            then y = x0 by FUNCOP_1: 7, A26;

            hence thesis by TARSKI:def 1;

          end;

          let y be object;

          assume y in {x0};

          then

           A27: y = x0 by TARSKI:def 1;

          

           A28: ( 0 + l) in NAT by ORDINAL1:def 12;

          (c . 0 ) = (s2 . ( 0 + l)) by NAT_1:def 3

          .= y by A27, FUNCOP_1: 7, A28;

          hence thesis by NFCONT_1: 6;

        end;

         A29:

        now

          let p be Real such that

           A30: 0 < p;

          reconsider n = 0 as Nat;

          take n;

          let m be Nat such that n <= m;

          

           A31: m in NAT by ORDINAL1:def 12;

          

           A32: (m + l) in NAT by ORDINAL1:def 12;

          x0 in N by NFCONT_1: 4;

          then ( rng c) c= ( dom f) by A2, A24, ZFMISC_1: 31;

          

          then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2: 109, A31

          .= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def 3

          .= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1: 7, A32

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

          .= 0 by NORMSP_1: 1;

          hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A30;

        end;

        then

         A33: (f /* c) is convergent;

        

         A34: ( rng (h + c)) c= N

        proof

          let y be object;

          assume

           A35: y in ( rng (h + c));

          then

          consider n be Nat such that

           A36: y = ((h + c) . n) by NFCONT_1: 6;

          reconsider y1 = y as Point of S by A35;

          ((h + c) . n) = ((((s1 - s2) + s2) ^\ l) . n) by A18, Th15

          .= (((s1 - s2) + s2) . (n + l)) by NAT_1:def 3

          .= (((s1 - s2) . (n + l)) + (s2 . (n + l))) by NORMSP_1:def 2

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

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

          .= ((s1 . (n + l)) - ( 0. S)) by RLVECT_1: 15

          .= (s1 . (l + n)) by RLVECT_1: 13;

          then ||.(((h + c) . n) - x0).|| < g by A10, NAT_1: 12;

          then y1 in { z where z be Point of S : ||.(z - x0).|| < g } by A36;

          hence thesis by A5;

        end;

        then

         A37: ((f /* (h + c)) - (f /* c)) is convergent by A17, A1, A2, A24, Th34;

        then (((f /* (h + c)) - (f /* c)) + (f /* c)) is convergent by A33, NORMSP_1: 19;

        hence (f /* s1) is convergent by A23, LOPBAN_3: 10;

        

         A38: ( lim ((f /* (h + c)) - (f /* c))) = ( 0. T) by A17, A1, A2, A24, A34, Th34;

        ( lim (f /* c)) = (f /. x0) by A29, A33, NORMSP_1:def 7;

        

        then ( lim (((f /* (h + c)) - (f /* c)) + (f /* c))) = (( 0. T) + (f /. x0)) by A37, A38, A33, NORMSP_1: 25

        .= (f /. x0) by RLVECT_1: 4;

        hence (f /. x0) = ( lim (f /* s1)) by A37, A33, A23, LOPBAN_3: 11, NORMSP_1: 19;

      end;

      x0 in N by NFCONT_1: 4;

      hence thesis by A2, A3, Th27;

    end;

    theorem :: NDIFF_1:45

    f is_differentiable_on X implies f is_continuous_on X by Th44;

    theorem :: NDIFF_1:46

    for Z be Subset of S st Z is open holds (f is_differentiable_on X & Z c= X implies f is_differentiable_on Z)

    proof

      let Z be Subset of S such that

       A1: Z is open;

      assume that

       A2: f is_differentiable_on X and

       A3: Z c= X;

      X c= ( dom f) by A2;

      hence

       A4: Z c= ( dom f) by A3;

      let x0;

      assume

       A5: x0 in Z;

      then

      consider N1 be Neighbourhood of x0 such that

       A6: N1 c= Z by A1, Th2;

      (f | X) is_differentiable_in x0 by A2, A3, A5;

      then

      consider N be Neighbourhood of x0 such that

       A7: N c= ( dom (f | X)) and

       A8: ex L, R st for x be Point of S st x in N holds (((f | X) /. x) - ((f | X) /. x0)) = ((L . (x - x0)) + (R /. (x - x0)));

      consider N2 be Neighbourhood of x0 such that

       A9: N2 c= N and

       A10: N2 c= N1 by Th1;

      

       A11: N2 c= Z by A6, A10;

      take N2;

      ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61;

      then ( dom (f | X)) c= ( dom f) by XBOOLE_1: 17;

      then N c= ( dom f) by A7;

      then N2 c= ( dom f) by A9;

      then N2 c= (( dom f) /\ Z) by A11, XBOOLE_1: 19;

      hence

       A12: N2 c= ( dom (f | Z)) by RELAT_1: 61;

      consider L, R such that

       A13: for x be Point of S st x in N holds (((f | X) /. x) - ((f | X) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A8;

      take L, R;

      let x be Point of S;

      assume

       A14: x in N2;

      then (((f | X) /. x) - ((f | X) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A9, A13;

      then

       A15: (((f | X) /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A3, A4, A5, PARTFUN2: 17;

      x in N by A9, A14;

      then ((f /. x) - (f /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A7, A15, PARTFUN2: 15;

      then ((f /. x) - ((f | Z) /. x0)) = ((L . (x - x0)) + (R /. (x - x0))) by A4, A5, PARTFUN2: 17;

      hence thesis by A12, A14, PARTFUN2: 15;

    end;

    theorem :: NDIFF_1:47

    f is_differentiable_in x0 implies ex N be Neighbourhood of x0 st N c= ( dom f) & ex R st (R /. ( 0. S)) = ( 0. T) & R is_continuous_in ( 0. S) & for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((( diff (f,x0)) . (x - x0)) + (R /. (x - x0)))

    proof

      assume f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A1: N c= ( dom f) and

       A2: ex R st for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((( diff (f,x0)) . (x - x0)) + (R /. (x - x0))) by Def7;

      take N;

      ex R st (R /. ( 0. S)) = ( 0. T) & R is_continuous_in ( 0. S) & for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((( diff (f,x0)) . (x - x0)) + (R /. (x - x0)))

      proof

        ( R_NormSpace_of_BoundedLinearOperators (S,T)) = NORMSTR (# ( BoundedLinearOperators (S,T)), ( Zero_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Add_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( Mult_ (( BoundedLinearOperators (S,T)),( R_VectorSpace_of_LinearOperators (S,T)))), ( BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;

        then

        reconsider L = ( diff (f,x0)) as Element of ( BoundedLinearOperators (S,T));

        consider R such that

         A3: for x be Point of S st x in N holds ((f /. x) - (f /. x0)) = ((( diff (f,x0)) . (x - x0)) + (R /. (x - x0))) by A2;

        take R;

        ((f /. x0) - (f /. x0)) = ((L . (x0 - x0)) + (R /. (x0 - x0))) by A3, NFCONT_1: 4;

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

        then ( 0. T) = ((L . ( 0. S)) + (R /. (x0 - x0))) by RLVECT_1: 15;

        then

         A4: ( 0. T) = ((L . ( 0. S)) + (R /. ( 0. S))) by RLVECT_1: 15;

        (L . ( 0. S)) = (( modetrans (L,S,T)) . ( 0. S)) by LOPBAN_1:def 11

        .= (( modetrans (L,S,T)) . ( 0 * ( 0. S))) by RLVECT_1: 10

        .= ( 0 * (( modetrans (L,S,T)) . ( 0. S))) by LOPBAN_1:def 5

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

        hence

         A5: (R /. ( 0. S)) = ( 0. T) by A4, RLVECT_1: 4;

         A6:

        now

          let s1 be sequence of S;

          assume that ( rng s1) c= ( dom R) and

           A7: s1 is convergent & ( lim s1) = ( 0. S) and

           A8: for n be Nat holds (s1 . n) <> ( 0. S);

          

           A9: s1 is ( 0. S) -convergent sequence of S by A7, Def4;

          s1 is non-zero by A8, Th7;

          hence (R /* s1) is convergent & ( lim (R /* s1)) = (R /. ( 0. S)) by A5, A9, Th24;

        end;

        R is total by Def5;

        then ( dom R) = the carrier of S by PARTFUN1:def 2;

        hence thesis by A3, A6, Th27;

      end;

      hence thesis by A1;

    end;

    definition

      let S be non trivial RealNormSpace, T;

      let IT be PartFunc of S, T;

      :: original: RestFunc-like

      redefine

      :: NDIFF_1:def10

      attr IT is RestFunc-like means IT is total & for h be non-zero( 0. S) -convergent sequence of S holds (( ||.h.|| " ) (#) (IT /* h)) is convergent & ( lim (( ||.h.|| " ) (#) (IT /* h))) = ( 0. T);

      correctness ;

    end