ndiff_2.miz



    begin

    reserve p for Real;

    reserve S,T for RealNormSpace;

    reserve x0 for Point of S;

    reserve f for PartFunc of S, T;

    reserve c for constant sequence of S;

    reserve R for RestFunc of S, T;

    definition

      let X,Y,Z be RealNormSpace;

      let f be Element of ( BoundedLinearOperators (X,Y));

      let g be Element of ( BoundedLinearOperators (Y,Z));

      :: NDIFF_2:def1

      func g * f -> Element of ( BoundedLinearOperators (X,Z)) equals (( modetrans (g,Y,Z)) * ( modetrans (f,X,Y)));

      correctness

      proof

        (( modetrans (g,Y,Z)) * ( modetrans (f,X,Y))) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

        hence thesis by LOPBAN_1:def 9;

      end;

    end

    definition

      let X,Y,Z be RealNormSpace;

      let f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      let g be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      :: NDIFF_2:def2

      func g * f -> Point of ( R_NormSpace_of_BoundedLinearOperators (X,Z)) equals (( modetrans (g,Y,Z)) * ( modetrans (f,X,Y)));

      correctness

      proof

        ( R_NormSpace_of_BoundedLinearOperators (X,Z)) = NORMSTR (# ( BoundedLinearOperators (X,Z)), ( Zero_ (( BoundedLinearOperators (X,Z)),( R_VectorSpace_of_LinearOperators (X,Z)))), ( Add_ (( BoundedLinearOperators (X,Z)),( R_VectorSpace_of_LinearOperators (X,Z)))), ( Mult_ (( BoundedLinearOperators (X,Z)),( R_VectorSpace_of_LinearOperators (X,Z)))), ( BoundedLinearOperatorsNorm (X,Z)) #) & (( modetrans (g,Y,Z)) * ( modetrans (f,X,Y))) is Lipschitzian LinearOperator of X, Z by LOPBAN_1:def 14, LOPBAN_2: 2;

        hence thesis by LOPBAN_1:def 9;

      end;

    end

    theorem :: NDIFF_2:1

    

     Th1: for x0 be Point of S st f is_differentiable_in x0 holds ex N be Neighbourhood of x0 st (N c= ( dom f) & for z be Point of S holds for h be 0 -convergent non-zero Real_Sequence holds for c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & (( diff (f,x0)) . z) = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))))

    proof

      let x0 be Point of S;

      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 (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))) by NDIFF_1: 47;

      consider R such that

       A3: (R /. ( 0. S)) = ( 0. T) and R is_continuous_in ( 0. S) and

       A4: 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;

      now

        let z be Point of S;

        let h be 0 -convergent non-zero Real_Sequence;

        let c such that

         A5: ( rng c) = {x0} and

         A6: ( rng ((h * z) + c)) c= N;

        

         A7: ((( abs h) " ) (#) (R /* (h * z))) is convergent & ( lim ((( abs h) " ) (#) (R /* (h * z)))) = ( 0. T)

        proof

          now

            per cases ;

              case

               A8: z = ( 0. S);

              for n be Nat holds (((( abs h) " ) (#) (R /* (h * z))) . n) = ( 0. T)

              proof

                let n be Nat;

                R is total by NDIFF_1:def 5;

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

                then

                 A9: ( rng (h * z)) c= ( dom R);

                

                 A10: n in NAT by ORDINAL1:def 12;

                

                thus (((( abs h) " ) (#) (R /* (h * z))) . n) = (((( abs h) " ) . n) * ((R /* (h * z)) . n)) by NDIFF_1:def 2

                .= (((( abs h) . n) " ) * ((R /* (h * z)) . n)) by VALUED_1: 10

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

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

                .= (( |.(h . n).| " ) * (R /. ((h . n) * ( 0. S)))) by A8, NDIFF_1:def 3

                .= (( |.(h . n).| " ) * (R /. ( 0. S))) by RLVECT_1: 10

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

              end;

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

              hence thesis by NDIFF_1: 18;

            end;

              case z <> ( 0. S);

              then

               A11: (h * z) is non-zero( 0. S) -convergent by NDIFF_1: 21;

              then

              reconsider s = (h * z) as ( 0. S) -convergent sequence of S;

              now

                let n be Element of NAT ;

                R is total by NDIFF_1:def 5;

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

                then

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

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

                then

                 A13: |.(h . n).| <> 0 by COMPLEX1: 47;

                (s . n) <> ( 0. S) by NDIFF_1: 7, A11;

                then

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

                 ||.(s . n).|| = ||.((h . n) * z).|| by NDIFF_1:def 3

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

                

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

                .= (1 * ||.z.||) by A13, XCMPLX_0:def 7

                .= ||.z.||;

                

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

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

                .= (( |.(h . n).| " ) * 1) by A14, XCMPLX_1: 60

                .= ( |.(h . n).| " );

                then

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

                R is total by NDIFF_1:def 5;

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

                then

                 A16: ( rng (h * z)) c= ( dom R);

                

                thus (((( abs h) " ) (#) (R /* (h * z))) . n) = (((( abs h) " ) . n) * ((R /* (h * z)) . n)) by NDIFF_1:def 2

                .= (((( abs h) . n) " ) * ((R /* (h * z)) . n)) by VALUED_1: 10

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

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

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

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

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

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

                .= (( ||.z.|| * (( ||.s.|| " ) (#) (R /* s))) . n) by NORMSP_1:def 5;

              end;

              then

               A17: ((( abs h) " ) (#) (R /* (h * z))) = ( ||.z.|| * (( ||.s.|| " ) (#) (R /* s))) by FUNCT_2: 63;

              

               A18: (( ||.s.|| " ) (#) (R /* s)) is convergent by A11, NDIFF_1:def 5;

              hence ((( abs h) " ) (#) (R /* (h * z))) is convergent by A17, NORMSP_1: 22;

              ( lim (( ||.s.|| " ) (#) (R /* s))) = ( 0. T) by A11, NDIFF_1:def 5;

              

              hence ( lim ((( abs h) " ) (#) (R /* (h * z)))) = ( ||.z.|| * ( 0. T)) by A17, A18, NORMSP_1: 28

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

            end;

          end;

          hence thesis;

        end;

         A19:

        now

          let e be Real;

          assume 0 < e;

          then

          consider m be Nat such that

           A20: for n be Nat st m <= n holds ||.((((( abs h) " ) (#) (R /* (h * z))) . n) - ( 0. T)).|| < e by A7, NORMSP_1:def 7;

          now

            let n be Nat such that

             A21: m <= n;

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

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

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

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

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

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

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

            .= ||.(((( abs h) " ) . n) * ((R /* (h * z)) . n)).|| by SEQ_1: 54

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

            .= ||.((((( abs h) " ) (#) (R /* (h * z))) . n) - ( 0. T)).|| by RLVECT_1: 13;

            hence ||.((((h " ) (#) (R /* (h * z))) . n) - ( 0. T)).|| < e by A20, A21;

          end;

          hence ex m be Nat st for n be Nat st m <= n holds ||.((((h " ) (#) (R /* (h * z))) . n) - ( 0. T)).|| < e;

        end;

        x0 in N by NFCONT_1: 4;

        then

         A22: ( rng c) c= ( dom f) by A1, A5, ZFMISC_1: 31;

        

         A23: for n be Nat holds ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - (( diff (f,x0)) . z)).|| = ||.(((h " ) (#) (R /* (h * z))) . n).||

        proof

          R is total by NDIFF_1:def 5;

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

          then

           A24: ( rng (h * z)) c= ( dom 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 = ( diff (f,x0)) as Element of ( BoundedLinearOperators (S,T));

          let n be Nat;

          

           A25: n in NAT by ORDINAL1:def 12;

          

           A26: (h . n) <> 0 by SEQ_1: 5;

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

          then (c . n) in ( rng c) by FUNCT_1: 3, A25;

          then

           A27: (c . n) = x0 by A5, TARSKI:def 1;

          ( dom ((h * z) + c)) = NAT by FUNCT_2:def 1;

          then (((h * z) + c) . n) in ( rng ((h * z) + c)) by FUNCT_1: 3, A25;

          then (((h * z) + c) . n) in N by A6;

          then (((h * z) . n) + (c . n)) in N by NORMSP_1:def 2;

          then

           A28: (((h . n) * z) + x0) in N by A27, NDIFF_1:def 3;

          ((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - (( diff (f,x0)) . z)) = ((((h " ) . n) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - (( diff (f,x0)) . z)) by NDIFF_1:def 2

          .= ((((h . n) " ) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - (( diff (f,x0)) . z)) by VALUED_1: 10

          .= ((((h . n) " ) * (((f /* ((h * z) + c)) . n) - ((f /* c) . n))) - (( diff (f,x0)) . z)) by NORMSP_1:def 3

          .= ((((h . n) " ) * ((f /. (((h * z) + c) . n)) - ((f /* c) . n))) - (( diff (f,x0)) . z)) by A1, A6, FUNCT_2: 109, XBOOLE_1: 1, A25

          .= ((((h . n) " ) * ((f /. (((h * z) + c) . n)) - (f /. (c . n)))) - (( diff (f,x0)) . z)) by A22, FUNCT_2: 109, A25

          .= ((((h . n) " ) * ((f /. (((h * z) . n) + (c . n))) - (f /. (c . n)))) - (( diff (f,x0)) . z)) by NORMSP_1:def 2

          .= ((((h . n) " ) * ((f /. (((h . n) * z) + (c . n))) - (f /. (c . n)))) - (( diff (f,x0)) . z)) by NDIFF_1:def 3

          .= ((((h . n) " ) * ((( diff (f,x0)) . ((((h . n) * z) + x0) - x0)) + (R /. ((((h . n) * z) + x0) - x0)))) - (( diff (f,x0)) . z)) by A4, A27, A28

          .= ((((h . n) " ) * ((( diff (f,x0)) . (((h . n) * z) + (x0 - x0))) + (R /. ((((h . n) * z) + x0) - x0)))) - (( diff (f,x0)) . z)) by RLVECT_1:def 3

          .= ((((h . n) " ) * ((( diff (f,x0)) . (((h . n) * z) + (x0 - x0))) + (R /. (((h . n) * z) + (x0 - x0))))) - (( diff (f,x0)) . z)) by RLVECT_1:def 3

          .= ((((h . n) " ) * ((( diff (f,x0)) . (((h . n) * z) + ( 0. S))) + (R /. (((h . n) * z) + (x0 - x0))))) - (( diff (f,x0)) . z)) by RLVECT_1: 15

          .= ((((h . n) " ) * ((( diff (f,x0)) . (((h . n) * z) + ( 0. S))) + (R /. (((h . n) * z) + ( 0. S))))) - (( diff (f,x0)) . z)) by RLVECT_1: 15

          .= ((((h . n) " ) * ((( diff (f,x0)) . ((h . n) * z)) + (R /. (((h . n) * z) + ( 0. S))))) - (( diff (f,x0)) . z)) by RLVECT_1: 4

          .= ((((h . n) " ) * ((( diff (f,x0)) . ((h . n) * z)) + (R /. ((h . n) * z)))) - (( diff (f,x0)) . z)) by RLVECT_1: 4

          .= (((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * (( diff (f,x0)) . ((h . n) * z)))) - (( diff (f,x0)) . z)) by RLVECT_1:def 5

          .= (((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * (( modetrans (L,S,T)) . ((h . n) * z)))) - (( diff (f,x0)) . z)) by LOPBAN_1:def 11

          .= (((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * ((h . n) * (( modetrans (L,S,T)) . z)))) - (( diff (f,x0)) . z)) by LOPBAN_1:def 5

          .= (((((h . n) " ) * (R /. ((h . n) * z))) + (((h . n) " ) * ((h . n) * (L . z)))) - (( diff (f,x0)) . z)) by LOPBAN_1:def 11

          .= (((((h . n) " ) * (R /. ((h . n) * z))) + ((((h . n) " ) * (h . n)) * (( diff (f,x0)) . z))) - (( diff (f,x0)) . z)) by RLVECT_1:def 7

          .= (((((h . n) " ) * (R /. ((h . n) * z))) + (1 * (( diff (f,x0)) . z))) - (( diff (f,x0)) . z)) by A26, XCMPLX_0:def 7

          .= (((((h . n) " ) * (R /. ((h . n) * z))) + (( diff (f,x0)) . z)) - (( diff (f,x0)) . z)) by RLVECT_1:def 8

          .= ((((h . n) " ) * (R /. ((h . n) * z))) + ((( diff (f,x0)) . z) - (( diff (f,x0)) . z))) by RLVECT_1:def 3

          .= ((((h . n) " ) * (R /. ((h . n) * z))) + ( 0. T)) by RLVECT_1: 15

          .= (((h . n) " ) * (R /. ((h . n) * z))) by RLVECT_1: 4

          .= (((h " ) . n) * (R /. ((h . n) * z))) by VALUED_1: 10

          .= (((h " ) . n) * (R /. ((h * z) . n))) by NDIFF_1:def 3

          .= (((h " ) . n) * ((R /* (h * z)) . n)) by A24, FUNCT_2: 109, A25

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

          hence thesis;

        end;

         A29:

        now

          let e be Real;

          assume 0 < e;

          then

          consider m be Nat such that

           A30: for n be Nat st m <= n holds ||.((((h " ) (#) (R /* (h * z))) . n) - ( 0. T)).|| < e by A19;

          now

            let n be Nat;

            assume m <= n;

            then ||.((((h " ) (#) (R /* (h * z))) . n) - ( 0. T)).|| < e by A30;

            then ||.(((h " ) (#) (R /* (h * z))) . n).|| < e by RLVECT_1: 13;

            hence ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - (( diff (f,x0)) . z)).|| < e by A23;

          end;

          hence ex m be Nat st for n be Nat st m <= n holds ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - (( diff (f,x0)) . z)).|| < e;

        end;

        hence ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent by NORMSP_1:def 6;

        hence ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) = (( diff (f,x0)) . z) by A29, NORMSP_1:def 7;

      end;

      hence thesis by A1;

    end;

    theorem :: NDIFF_2:2

    for x0 be Point of S st f is_differentiable_in x0 holds for z be Point of S holds for h be 0 -convergent non-zero Real_Sequence holds for c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= ( dom f) holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & (( diff (f,x0)) . z) = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))))

    proof

      let x0 be Point of S;

      assume f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A1: N c= ( dom f) and

       A2: for z be Point of S holds for h be 0 -convergent non-zero Real_Sequence holds for c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & (( diff (f,x0)) . z) = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) by Th1;

      let z be Point of S;

      let h be 0 -convergent non-zero Real_Sequence;

      let c such that

       A3: ( rng c) = {x0} and

       A4: ( rng ((h * z) + c)) c= ( dom f);

      x0 in N by NFCONT_1: 4;

      then

       A5: ( rng c) c= ( dom f) by A3, A1, ZFMISC_1: 31;

      consider g be Real such that

       A6: 0 < g and

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

      

       A8: for n be Element of NAT holds (c . n) = x0

      proof

        let n be Element of NAT ;

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

        hence thesis by A3, TARSKI:def 1;

      end;

      ex n be Element of NAT st ( rng (((h ^\ n) * z) + c)) c= N

      proof

         A9:

        now

          let p;

          assume

           A10: 0 < p;

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

          proof

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

            

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

            

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

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

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

            hence thesis by A10, A12, XCMPLX_1: 87;

          end;

          then

          consider pp be Real such that

           A13: pp > 0 and

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

          h is convergent & ( lim h) = 0 ;

          then

          consider n be Nat such that

           A15: for m be Nat st n <= m holds |.((h . m) - 0 ).| < pp by A13, SEQ_2:def 7;

          take n;

          let m be Nat;

          assume n <= m;

          then

           A16: |.((h . m) - 0 ).| < pp by A15;

          

           A17: ||.(((h * z) . m) - ( 0. S)).|| = ||.(((h . m) * z) - ( 0. S)).|| by NDIFF_1:def 3

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

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

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

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

          hence ||.(((h * z) . m) - ( 0. S)).|| < p by A14, A17, XXREAL_0: 2;

        end;

        then

         A18: (h * z) is convergent by NORMSP_1:def 6;

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

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

        then

         A19: ( lim c) = x0 by NDIFF_1: 18;

        

         A20: c is convergent by NDIFF_1: 18;

        then

         A21: ((h * z) + c) is convergent by A18, NORMSP_1: 19;

        ( lim (h * z)) = ( 0. S) by A9, A18, NORMSP_1:def 7;

        

        then ( lim ((h * z) + c)) = (( 0. S) + x0) by A20, A19, A18, NORMSP_1: 25

        .= x0 by RLVECT_1: 4;

        then

        consider n be Nat such that

         A22: for m be Nat st n <= m holds ||.((((h * z) + c) . m) - x0).|| < g by A6, A21, NORMSP_1:def 7;

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

        take n;

        let y be object;

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

        then

        consider m be Nat such that

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

        

         A24: (n + m) in NAT by ORDINAL1:def 12;

        

         A25: m in NAT by ORDINAL1:def 12;

        reconsider y1 = y as Point of S by A23;

         ||.((((h * z) + c) . (n + m)) - x0).|| < g by A22, NAT_1: 11;

        then ||.((((h * z) . (n + m)) + (c . (n + m))) - x0).|| < g by NORMSP_1:def 2;

        then ||.((((h * z) . (n + m)) + x0) - x0).|| < g by A8, A24;

        then ||.((((h * z) . (n + m)) + (c . m)) - x0).|| < g by A8, A25;

        then ||.((((h . (n + m)) * z) + (c . m)) - x0).|| < g by NDIFF_1:def 3;

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

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

        then ||.(((((h ^\ n) * z) + c) . m) - x0).|| < g by NORMSP_1:def 2;

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

        hence thesis by A7;

      end;

      then

      consider n be Element of NAT such that

       A26: ( rng (((h ^\ n) * z) + c)) c= N;

       A27:

      now

        let m be Element of NAT ;

        

        thus ((((h * z) + c) ^\ n) . m) = (((h * z) + c) . (n + m)) by NAT_1:def 3

        .= (((h * z) . (n + m)) + (c . (n + m))) by NORMSP_1:def 2

        .= (((h * z) . (n + m)) + x0) by A8

        .= (((h * z) . (n + m)) + (c . m)) by A8

        .= (((h . (n + m)) * z) + (c . m)) by NDIFF_1:def 3

        .= ((((h ^\ n) . m) * z) + (c . m)) by NAT_1:def 3

        .= ((((h ^\ n) * z) . m) + (c . m)) by NDIFF_1:def 3

        .= ((((h ^\ n) * z) + c) . m) by NORMSP_1:def 2;

      end;

      now

        let m be Element of NAT ;

        

         A28: (((f /* ((h * z) + c)) ^\ n) . m) = ((f /* ((h * z) + c)) . (n + m)) by NAT_1:def 3

        .= (f /. (((h * z) + c) . (n + m))) by A4, FUNCT_2: 109

        .= (f /. ((((h * z) + c) ^\ n) . m)) by NAT_1:def 3

        .= (f /. ((((h ^\ n) * z) + c) . m)) by A27;

        

        thus ((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n) . m) = (((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . (n + m)) by NAT_1:def 3

        .= (((h " ) . (n + m)) * (((f /* ((h * z) + c)) - (f /* c)) . (n + m))) by NDIFF_1:def 2

        .= (((h . (n + m)) " ) * (((f /* ((h * z) + c)) - (f /* c)) . (n + m))) by VALUED_1: 10

        .= ((((h ^\ n) . m) " ) * (((f /* ((h * z) + c)) - (f /* c)) . (n + m))) by NAT_1:def 3

        .= ((((h ^\ n) . m) " ) * (((f /* ((h * z) + c)) . (n + m)) - ((f /* c) . (n + m)))) by NORMSP_1:def 3

        .= ((((h ^\ n) . m) " ) * ((((f /* ((h * z) + c)) ^\ n) . m) - ((f /* c) . (n + m)))) by NAT_1:def 3

        .= ((((h ^\ n) . m) " ) * ((f /. ((((h ^\ n) * z) + c) . m)) - (f /. (c . (n + m))))) by A5, A28, FUNCT_2: 109

        .= ((((h ^\ n) . m) " ) * ((f /. ((((h ^\ n) * z) + c) . m)) - (f /. x0))) by A8

        .= ((((h ^\ n) . m) " ) * ((f /. ((((h ^\ n) * z) + c) . m)) - (f /. (c . m)))) by A8

        .= ((((h ^\ n) . m) " ) * ((f /. ((((h ^\ n) * z) + c) . m)) - ((f /* c) . m))) by A5, FUNCT_2: 109

        .= ((((h ^\ n) . m) " ) * (((f /* (((h ^\ n) * z) + c)) . m) - ((f /* c) . m))) by A1, A26, FUNCT_2: 109, XBOOLE_1: 1

        .= ((((h ^\ n) . m) " ) * (((f /* (((h ^\ n) * z) + c)) - (f /* c)) . m)) by NORMSP_1:def 3

        .= ((((h ^\ n) " ) . m) * (((f /* (((h ^\ n) * z) + c)) - (f /* c)) . m)) by VALUED_1: 10

        .= ((((h ^\ n) " ) (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) . m) by NDIFF_1:def 2;

      end;

      then

       A29: (((h ^\ n) " ) (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) = (((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ^\ n) by FUNCT_2: 63;

      (((h ^\ n) " ) (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c))) is convergent & (( diff (f,x0)) . z) = ( lim (((h ^\ n) " ) (#) ((f /* (((h ^\ n) * z) + c)) - (f /* c)))) by A3, A2, A26;

      hence thesis by A29, LOPBAN_3: 10, LOPBAN_3: 11;

    end;

    theorem :: NDIFF_2:3

    

     Th3: for x0 be Point of S holds for N be Neighbourhood of x0 st N c= ( dom f) holds for z be Point of S holds for dv be Point of T holds ((for h be 0 -convergent non-zero Real_Sequence holds for c st (( rng c) = {x0} & ( rng ((h * z) + c)) c= N) holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))))) iff for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e)

    proof

      let x0 be Point of S;

      let N be Neighbourhood of x0 such that

       A1: N c= ( dom f);

      let z be Point of S;

      let dv be Point of T;

       A2:

      now

        reconsider c = ( NAT --> x0) as sequence of S;

        assume

         A3: for h be 0 -convergent non-zero Real_Sequence holds for c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))));

        now

          let x be object;

          assume x in {x0};

          then x = x0 by TARSKI:def 1;

          then x = (c . 1);

          hence x in ( rng c) by NFCONT_1: 6;

        end;

        then

         A4: {x0} c= ( rng c);

        now

          let x be object;

          assume x in ( rng c);

          then

          consider n be Nat such that

           A5: x = (c . n) by NFCONT_1: 6;

          n in NAT by ORDINAL1:def 12;

          then x = x0 by FUNCOP_1: 7, A5;

          hence x in {x0} by TARSKI:def 1;

        end;

        then ( rng c) c= {x0};

        then

         A6: ( rng c) = {x0} by A4, XBOOLE_0:def 10;

        assume not (for r be Real st r > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r);

        then

        consider r be Real such that

         A7: r > 0 and

         A8: for d be Real st d > 0 holds ex h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N & not ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r;

        defpred P[ Nat, Real] means ex rr be Real st rr = $2 & |.rr.| < (1 / ($1 + 1)) & rr <> 0 & ((rr * z) + x0) in N & not ( ||.(((rr " ) * ((f /. ((rr * z) + x0)) - (f /. x0))) - dv).|| < r);

        

         A9: for n be Element of NAT holds ex h be Element of REAL st P[n, h]

        proof

          let n be Element of NAT ;

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

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

          then

          consider h be Real such that

           A10: |.h.| < (1 / (n + 1)) & h <> 0 & ((h * z) + x0) in N & not ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r by A8;

          h in REAL by XREAL_0:def 1;

          hence thesis by A10;

        end;

        consider h be Real_Sequence such that

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

         A12:

        now

          let p be Real;

          assume

           A13: 0 < p;

          consider n be Nat such that

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

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

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

          then

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

          take n;

          let m be Nat;

          assume n <= m;

          then

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

          m in NAT by ORDINAL1:def 12;

          then

           A17: P[m, (h . m)] by A11;

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

          then |.((h . m) - 0 ).| < (1 / (n + 1)) by A17, XXREAL_0: 2;

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

        end;

        then

         A18: h is convergent by SEQ_2:def 6;

        then

         A19: ( lim h) = 0 by A12, SEQ_2:def 7;

        for n be Nat holds (h . n) <> 0

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then P[n, (h . n)] by A11;

          hence thesis;

        end;

        then h is non-zero by SEQ_1: 5;

        then

        reconsider h as 0 -convergent non-zero Real_Sequence by A18, A19, FDIFF_1:def 1;

        now

          let x be object;

          assume x in ( rng ((h * z) + c));

          then

          consider n be Nat such that

           A20: x = (((h * z) + c) . n) by NFCONT_1: 6;

          

           A21: n in NAT by ORDINAL1:def 12;

          

           A22: x = (((h * z) . n) + (c . n)) by A20, NORMSP_1:def 2

          .= (((h . n) * z) + (c . n)) by NDIFF_1:def 3

          .= (((h . n) * z) + x0) by FUNCOP_1: 7, A21;

           P[n, (h . n)] by A11, A21;

          hence x in N by A22;

        end;

        then

         A23: ( rng ((h * z) + c)) c= N;

        then ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) by A3, A6;

        then

        consider n be Nat such that

         A24: for m be Nat st n <= m holds ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r by A7, NORMSP_1:def 7;

        x0 in N by NFCONT_1: 4;

        then

         A25: ( rng c) c= ( dom f) by A1, A6, ZFMISC_1: 31;

        

         A26: n in NAT by ORDINAL1:def 12;

        

         A27: P[n, (h . n)] by A11, A26;

         ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . n) - dv).|| = ||.((((h " ) . n) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - dv).|| by NDIFF_1:def 2

        .= ||.((((h . n) " ) * (((f /* ((h * z) + c)) - (f /* c)) . n)) - dv).|| by VALUED_1: 10

        .= ||.((((h . n) " ) * (((f /* ((h * z) + c)) . n) - ((f /* c) . n))) - dv).|| by NORMSP_1:def 3

        .= ||.((((h . n) " ) * (((f /* ((h * z) + c)) . n) - (f /. (c . n)))) - dv).|| by A25, FUNCT_2: 109, A26

        .= ||.((((h . n) " ) * (((f /* ((h * z) + c)) . n) - (f /. x0))) - dv).|| by FUNCOP_1: 7, A26

        .= ||.((((h . n) " ) * ((f /. (((h * z) + c) . n)) - (f /. x0))) - dv).|| by A1, A23, FUNCT_2: 109, A26, XBOOLE_1: 1

        .= ||.((((h . n) " ) * ((f /. (((h * z) . n) + (c . n))) - (f /. x0))) - dv).|| by NORMSP_1:def 2

        .= ||.((((h . n) " ) * ((f /. (((h * z) . n) + x0)) - (f /. x0))) - dv).|| by FUNCOP_1: 7, A26

        .= ||.((((h . n) " ) * ((f /. (((h . n) * z) + x0)) - (f /. x0))) - dv).|| by NDIFF_1:def 3;

        hence for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e by A24, A27;

      end;

      now

        assume

         A28: for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e;

        now

          let h be 0 -convergent non-zero Real_Sequence;

          let c such that

           A29: ( rng c) = {x0} and

           A30: ( rng ((h * z) + c)) c= N;

          

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

          x0 in N by NFCONT_1: 4;

          then

           A32: ( rng c) c= ( dom f) by A1, A29, ZFMISC_1: 31;

          

           A33: for n be Element of NAT holds (c . n) = x0

          proof

            let n be Element of NAT ;

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

            hence thesis by A29, TARSKI:def 1;

          end;

           A34:

          now

            let r be Real;

            assume r > 0 ;

            then

            consider d be Real such that

             A35: d > 0 and

             A36: for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < r by A28;

            consider n be Nat such that

             A37: for m be Nat st n <= m holds |.((h . m) - 0 ).| < d by A31, A35, SEQ_2:def 7;

            take n;

            thus for m be Nat st n <= m holds ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| < r

            proof

              let m be Nat;

              

               A38: m in NAT by ORDINAL1:def 12;

              

               A39: (h . m) <> 0 by SEQ_1: 5;

              assume n <= m;

              then

               A40: |.((h . m) - 0 ).| < d by A37;

              (((h * z) + c) . m) in ( rng ((h * z) + c)) by NFCONT_1: 6;

              then (((h * z) + c) . m) in N by A30;

              then (((h * z) . m) + (c . m)) in N by NORMSP_1:def 2;

              then (((h . m) * z) + (c . m)) in N by NDIFF_1:def 3;

              then

               A41: (((h . m) * z) + x0) in N by A33, A38;

               ||.((((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) . m) - dv).|| = ||.((((h " ) . m) * (((f /* ((h * z) + c)) - (f /* c)) . m)) - dv).|| by NDIFF_1:def 2

              .= ||.((((h . m) " ) * (((f /* ((h * z) + c)) - (f /* c)) . m)) - dv).|| by VALUED_1: 10

              .= ||.((((h . m) " ) * (((f /* ((h * z) + c)) . m) - ((f /* c) . m))) - dv).|| by NORMSP_1:def 3

              .= ||.((((h . m) " ) * (((f /* ((h * z) + c)) . m) - (f /. (c . m)))) - dv).|| by A32, FUNCT_2: 109, A38

              .= ||.((((h . m) " ) * (((f /* ((h * z) + c)) . m) - (f /. x0))) - dv).|| by A33, A38

              .= ||.((((h . m) " ) * ((f /. (((h * z) + c) . m)) - (f /. x0))) - dv).|| by A1, A30, FUNCT_2: 109, XBOOLE_1: 1, A38

              .= ||.((((h . m) " ) * ((f /. (((h * z) . m) + (c . m))) - (f /. x0))) - dv).|| by NORMSP_1:def 2

              .= ||.((((h . m) " ) * ((f /. (((h * z) . m) + x0)) - (f /. x0))) - dv).|| by A33, A38

              .= ||.((((h . m) " ) * ((f /. (((h . m) * z) + x0)) - (f /. x0))) - dv).|| by NDIFF_1:def 3;

              hence thesis by A36, A40, A39, A41;

            end;

          end;

          hence ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent by NORMSP_1:def 6;

          hence ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) = dv by A34, NORMSP_1:def 7;

        end;

        hence for h be 0 -convergent non-zero Real_Sequence holds for c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))));

      end;

      hence thesis by A2;

    end;

    definition

      let S, T;

      let f;

      let x0 be Point of S;

      let z be Point of S;

      :: NDIFF_2:def3

      pred f is_Gateaux_differentiable_in x0,z means ex N be Neighbourhood of x0 st N c= ( dom f) & ex dv be Point of T st for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e;

    end

    theorem :: NDIFF_2:4

    

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

    proof

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

      proof

        let X be RealNormSpace;

        let x,y be Point of X;

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

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

        now

          assume x <> y;

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

          hence 0 < ||.(x - y).|| by NORMSP_1: 4;

        end;

        hence thesis;

      end;

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

      proof

        let X be RealNormSpace;

        let x,y be Point of X;

        

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

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

      end;

      

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

      proof

        let X be RealNormSpace;

        let x,y,z be Point of X;

        let e be Real such that e > 0 ;

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

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

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

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

        hence thesis;

      end;

      

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

      proof

        let X be RealNormSpace;

        let x,y,z be Point of X;

        let e be Real such that

         A3: e > 0 ;

        assume that

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

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

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

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

        hence thesis by A1, A3, A4;

      end;

      

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

      proof

        let X be RealNormSpace;

        let x be Point of X such that

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

        now

          assume x <> ( 0. X);

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

          then 0 < ||.x.|| by NORMSP_1: 4;

          hence contradiction by A7;

        end;

        hence thesis;

      end;

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

      proof

        let X be RealNormSpace;

        let x,y be Point of X;

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

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

        hence thesis by RLVECT_1: 21;

      end;

      hence thesis by A1, A2, A6, NORMSP_1: 6;

    end;

    definition

      let S, T;

      let f;

      let x0 be Point of S;

      let z be Point of S;

      assume

       A1: f is_Gateaux_differentiable_in (x0,z);

      :: NDIFF_2:def4

      func Gateaux_diff (f,x0,z) -> Point of T means

      : Def4: ex N be Neighbourhood of x0 st N c= ( dom f) & for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - it ).|| < e;

      existence by A1;

      uniqueness

      proof

        let dv1,dv2 be Point of T;

        assume that

         A2: ex N1 be Neighbourhood of x0 st N1 c= ( dom f) & for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N1 holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e and

         A3: ex N2 be Neighbourhood of x0 st N2 c= ( dom f) & for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N2 holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e;

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

         A4: for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N2 holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < e by A3;

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

         A5: for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N1 holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < e by A2;

        now

          let e be Real such that

           A6: e > 0 ;

          

           A7: 0 < (e / 2) by A6, XREAL_1: 215;

          then

          consider d1 be Real such that

           A8: d1 > 0 and

           A9: for h be Real st |.h.| < d1 & h <> 0 & ((h * z) + x0) in N1 holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < (e / 2) by A5;

          consider d2 be Real such that

           A10: d2 > 0 and

           A11: for h be Real st |.h.| < d2 & h <> 0 & ((h * z) + x0) in N2 holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < (e / 2) by A4, A7;

          ex h be Real st h <> 0 & |.h.| < d1 & |.h.| < d2 & ((h * z) + x0) in N1 & ((h * z) + x0) in N2

          proof

            set d3 = ( min (d1,d2));

            consider N0 be Neighbourhood of x0 such that

             A12: N0 c= N1 & N0 c= N2 by NDIFF_1: 1;

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

            set h = ( min ((1 / (n1 + 1)),(d3 / 2)));

            take h;

            

             A16: h <= (d3 / 2) by XXREAL_0: 17;

            

             A17: 0 < d3 by A8, A10, XXREAL_0: 15;

            then

             A18: 0 < (d3 / 2) by XREAL_1: 215;

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

            then

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

            hence h <> 0 by A18, XXREAL_0: 15;

            

             A20: 0 < h by A18, A19, XXREAL_0: 15;

            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

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

            

             A22: ||.(((h * z) + x0) - x0).|| = ||.((h * z) + (x0 - x0)).|| by RLVECT_1:def 3

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

            .= ||.(h * z).|| by RLVECT_1: 4

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

            .= (h * ||.z.||) by A20, ABSVALUE:def 1;

            

             A23: (d3 / 2) < d3 by A17, XREAL_1: 216;

            d3 <= d2 by XXREAL_0: 17;

            then (d3 / 2) < d2 by A23, XXREAL_0: 2;

            then

             A24: h < d2 by A16, XXREAL_0: 2;

            d3 <= d1 by XXREAL_0: 17;

            then (d3 / 2) < d1 by A23, XXREAL_0: 2;

            then h < d1 by A16, XXREAL_0: 2;

            hence |.h.| < d1 & |.h.| < d2 by A20, A24, ABSVALUE:def 1;

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

            then

             A25: (h * ||.z.||) <= ((1 / (n1 + 1)) * ||.z.||) by XREAL_1: 64, XXREAL_0: 17;

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

            then

             A26: ( ||.z.|| / (1 + n1)) <= ( ||.z.|| / n1) by XREAL_1: 118;

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

            then ((1 / (1 + n1)) * ||.z.||) < g by A21, A26, XXREAL_0: 2;

            then ||.(((h * z) + x0) - x0).|| < g by A22, A25, XXREAL_0: 2;

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

            then ((h * z) + x0) in N0 by A14;

            hence thesis by A12;

          end;

          then

          consider h be Real such that

           A27: |.h.| < d1 and

           A28: |.h.| < d2 and

           A29: h <> 0 and

           A30: ((h * z) + x0) in N1 and

           A31: ((h * z) + x0) in N2;

           ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv1).|| < (e / 2) by A9, A27, A29, A30;

          then

           A32: ||.(dv1 - ((h " ) * ((f /. ((h * z) + x0)) - (f /. x0)))).|| < (e / 2) by Th4;

           ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv2).|| < (e / 2) by A11, A28, A29, A31;

          hence ||.(dv1 - dv2).|| < e by A6, A32, Th4;

        end;

        hence thesis by Th4;

      end;

    end

    theorem :: NDIFF_2:5

    for x0 be Point of S, z be Point of S holds (f is_Gateaux_differentiable_in (x0,z) iff ex N be Neighbourhood of x0 st (N c= ( dom f) & ex dv be Point of T st for h be 0 -convergent non-zero Real_Sequence holds for c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))))))

    proof

      let x0 be Point of S;

      let z be Point of S;

       A1:

      now

        assume ex N be Neighbourhood of x0 st (N c= ( dom f) & ex dv be Point of T st for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))));

        then

        consider N be Neighbourhood of x0 such that

         A2: N c= ( dom f) and

         A3: ex dv be Point of T st for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))));

        consider dv be Point of T such that

         A4: for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) by A3;

        for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - dv).|| < e by A2, A4, Th3;

        hence f is_Gateaux_differentiable_in (x0,z) by A2;

      end;

      now

        assume f is_Gateaux_differentiable_in (x0,z);

        then

        consider N be Neighbourhood of x0 such that

         A5: N c= ( dom f) and

         A6: for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - ( Gateaux_diff (f,x0,z))).|| < e by Def4;

        for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & ( Gateaux_diff (f,x0,z)) = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) by A5, A6, Th3;

        hence ex N be Neighbourhood of x0 st (N c= ( dom f) & ex dv be Point of T st for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & dv = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))))) by A5;

      end;

      hence thesis by A1;

    end;

    theorem :: NDIFF_2:6

    for x0 be Point of S st f is_differentiable_in x0 holds for z be Point of S holds (f is_Gateaux_differentiable_in (x0,z) & ( Gateaux_diff (f,x0,z)) = (( diff (f,x0)) . z) & ex N be Neighbourhood of x0 st (N c= ( dom f) & for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & ( Gateaux_diff (f,x0,z)) = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))))))

    proof

      let x0 be Point of S;

      assume f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A1: N c= ( dom f) and

       A2: for z be Point of S holds for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & (( diff (f,x0)) . z) = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) by Th1;

      let z be Point of S;

      

       A3: for h be 0 -convergent non-zero Real_Sequence, c st ( rng c) = {x0} & ( rng ((h * z) + c)) c= N holds ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) is convergent & (( diff (f,x0)) . z) = ( lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c)))) by A2;

      then

       A4: for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & ((h * z) + x0) in N holds ||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - (( diff (f,x0)) . z)).|| < e by A1, Th3;

      hence f is_Gateaux_differentiable_in (x0,z) by A1;

      hence ( Gateaux_diff (f,x0,z)) = (( diff (f,x0)) . z) by A1, A4, Def4;

      hence thesis by A1, A3;

    end;

    reserve U for RealNormSpace;

    theorem :: NDIFF_2:7

    

     Th7: for R be RestFunc of S, T st (R /. ( 0. S)) = ( 0. T) holds for e be Real st e > 0 holds ex d be Real st d > 0 & for h be Point of S st ||.h.|| < d holds ||.(R /. h).|| <= (e * ||.h.||)

    proof

      let R be RestFunc of S, T such that

       A1: (R /. ( 0. S)) = ( 0. T);

      let e be Real such that

       A2: e > 0 ;

      R is total by NDIFF_1:def 5;

      then

      consider d be Real such that

       A3: d > 0 and

       A4: for z be Point of S st z <> ( 0. S) & ||.z.|| < d holds (( ||.z.|| " ) * ||.(R /. z).||) < e by A2, NDIFF_1: 23;

      take d;

      now

        let h be Point of S such that

         A5: ||.h.|| < d;

        now

          per cases ;

            case

             A6: h <> ( 0. S);

            then 0 <= ||.h.|| & (( ||.h.|| " ) * ||.(R /. h).||) <= e by A4, A5, NORMSP_1: 4;

            then ( ||.h.|| * (( ||.h.|| " ) * ||.(R /. h).||)) <= ( ||.h.|| * e) by XREAL_1: 64;

            then

             A7: (( ||.h.|| * ( ||.h.|| " )) * ||.(R /. h).||) <= (e * ||.h.||);

             ||.h.|| <> 0 by A6, NORMSP_0:def 5;

            then (1 * ||.(R /. h).||) <= (e * ||.h.||) by A7, XCMPLX_0:def 7;

            hence ||.(R /. h).|| <= (e * ||.h.||);

          end;

            case

             A8: h = ( 0. S);

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

            then ( 0 * ||.h.||) <= (e * ||.h.||) by A2;

            hence ||.(R /. h).|| <= (e * ||.h.||) by A1, A8, NORMSP_0:def 6;

          end;

        end;

        hence ||.(R /. h).|| <= (e * ||.h.||);

      end;

      hence thesis by A3;

    end;

    theorem :: NDIFF_2:8

    for R be RestFunc of T, U st (R /. ( 0. T)) = ( 0. U) holds for L be Lipschitzian LinearOperator of S, T holds (R * L) is RestFunc of S, U

    proof

      let R be RestFunc of T, U such that

       A1: (R /. ( 0. T)) = ( 0. U);

      let L be Lipschitzian LinearOperator of S, T;

      consider K be Real such that

       A2: 0 <= K and

       A3: for h be Point of S holds ||.(L . h).|| <= (K * ||.h.||) by LOPBAN_1:def 8;

      

       A4: ( dom L) = the carrier of S by FUNCT_2:def 1;

      R is total by NDIFF_1:def 5;

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

      then

       A5: ( rng L) c= ( dom R);

      

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

       A7:

      now

        let e be Real;

        assume e > 0 ;

        then

         A8: ( 0 / (1 + K)) < (e / (1 + K)) by A2, XREAL_1: 74;

        set e1 = (e / (1 + K));

        consider d be Real such that

         A9: 0 < d and

         A10: for h be Point of T st ||.h.|| < d holds ||.(R /. h).|| <= (e1 * ||.h.||) by A1, A8, Th7;

        set d1 = (d / (1 + K));

         A11:

        now

          let h be Point of S such that

           A12: h <> ( 0. S) and

           A13: ||.h.|| < d1;

          

           A14: ||.(L . h).|| <= (K * ||.h.||) by A3;

          

           A15: ||.h.|| <> 0 by A12, NORMSP_0:def 5;

          then

           A16: ||.h.|| > 0 by NORMSP_1: 4;

          then (K * ||.h.||) < ((K + 1) * ||.h.||) by A6, XREAL_1: 68;

          then

           A17: ||.(L . h).|| < ((K + 1) * ||.h.||) by A14, XXREAL_0: 2;

          ((K + 1) * ||.h.||) < ((K + 1) * d1) by A2, A13, XREAL_1: 68;

          then ||.(L . h).|| < ((K + 1) * d1) by A17, XXREAL_0: 2;

          then ||.(L . h).|| < d by A2, XCMPLX_1: 87;

          then

           A18: ||.(R /. (L . h)).|| <= (e1 * ||.(L . h).||) by A10;

          

           A19: (R /. (L . h)) = (R /. (L /. h))

          .= ((R * L) /. h) by A4, A5, PARTFUN2: 5;

          (e1 * ||.(L . h).||) < (e1 * ((K + 1) * ||.h.||)) by A8, A17, XREAL_1: 68;

          then ||.(R /. (L . h)).|| < (e1 * ((K + 1) * ||.h.||)) by A18, XXREAL_0: 2;

          then (( ||.h.|| " ) * ||.((R * L) /. h).||) < (( ||.h.|| " ) * ((e1 * (K + 1)) * ||.h.||)) by A19, A16, XREAL_1: 68;

          then (( ||.h.|| " ) * ||.((R * L) /. h).||) < ((( ||.h.|| * ( ||.h.|| " )) * e1) * (K + 1));

          then (( ||.h.|| " ) * ||.((R * L) /. h).||) < ((1 * e1) * (K + 1)) by A15, XCMPLX_0:def 7;

          hence (( ||.h.|| " ) * ||.((R * L) /. h).||) < e by A2, XCMPLX_1: 87;

        end;

        ( 0 / (1 + K)) < (d / (1 + K)) by A2, A9, XREAL_1: 74;

        hence ex d1 be Real st d1 > 0 & for h be Point of S st h <> ( 0. S) & ||.h.|| < d1 holds (( ||.h.|| " ) * ||.((R * L) /. h).||) < e by A11;

      end;

      ( dom (R * L)) = ( dom L) by A5, RELAT_1: 27

      .= the carrier of S by FUNCT_2:def 1;

      then (R * L) is total by PARTFUN1:def 2;

      hence thesis by A7, NDIFF_1: 23;

    end;

    theorem :: NDIFF_2:9

    

     Th9: for R be RestFunc of S, T holds for L be Lipschitzian LinearOperator of T, U holds (L * R) is RestFunc of S, U

    proof

      let R be RestFunc of S, T;

      let L be Lipschitzian LinearOperator of T, U;

      consider K be Real such that

       A1: 0 <= K and

       A2: for z be Point of T holds ||.(L . z).|| <= (K * ||.z.||) by LOPBAN_1:def 8;

      ( dom L) = the carrier of T by FUNCT_2:def 1;

      then

       A3: ( rng R) c= ( dom L);

      

       A4: R is total by NDIFF_1:def 5;

      then

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

      

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

       A7:

      now

        let ee be Real such that

         A8: ee > 0 ;

        set e = (ee / 2);

        e > 0 by A8, XREAL_1: 215;

        then

         A9: ( 0 / (1 + K)) < (e / (1 + K)) by A1, XREAL_1: 74;

        set e1 = (e / (1 + K));

        R is total by NDIFF_1:def 5;

        then

        consider d be Real such that

         A10: 0 < d and

         A11: for h be Point of S st h <> ( 0. S) & ||.h.|| < d holds (( ||.h.|| " ) * ||.(R /. h).||) < e1 by A9, NDIFF_1: 23;

        

         A12: e < ee by A8, XREAL_1: 216;

        now

          let h be Point of S such that

           A13: h <> ( 0. S) and

           A14: ||.h.|| < d;

          (( ||.h.|| " ) * ||.(R /. h).||) < e1 by A11, A13, A14;

          then ((K + 1) * (( ||.h.|| " ) * ||.(R /. h).||)) <= ((K + 1) * e1) by A1, XREAL_1: 64;

          then

           A15: ((K + 1) * (( ||.h.|| " ) * ||.(R /. h).||)) <= e by A1, XCMPLX_1: 87;

           ||.h.|| <> 0 by A13, NORMSP_0:def 5;

          then

           A16: ||.h.|| > 0 by NORMSP_1: 4;

           0 <= ||.(R /. h).|| by NORMSP_1: 4;

          then

           A17: (K * ||.(R /. h).||) <= ((K + 1) * ||.(R /. h).||) by A6, XREAL_1: 64;

           ||.(L . (R /. h)).|| <= (K * ||.(R /. h).||) by A2;

          then ||.(L . (R /. h)).|| <= ((K + 1) * ||.(R /. h).||) by A17, XXREAL_0: 2;

          then (( ||.h.|| " ) * ||.(L . (R /. h)).||) <= (( ||.h.|| " ) * ((K + 1) * ||.(R /. h).||)) by A16, XREAL_1: 64;

          then

           A18: (( ||.h.|| " ) * ||.(L . (R /. h)).||) <= e by A15, XXREAL_0: 2;

          (L . (R /. h)) = (L /. (R /. h))

          .= ((L * R) /. h) by A5, A3, PARTFUN2: 5;

          hence (( ||.h.|| " ) * ||.((L * R) /. h).||) < ee by A12, A18, XXREAL_0: 2;

        end;

        hence ex d be Real st d > 0 & for h be Point of S st h <> ( 0. S) & ||.h.|| < d holds (( ||.h.|| " ) * ||.((L * R) /. h).||) < ee by A10;

      end;

      ( dom (L * R)) = ( dom R) by A3, RELAT_1: 27

      .= the carrier of S by A4, PARTFUN1:def 2;

      then (L * R) is total by PARTFUN1:def 2;

      hence thesis by A7, NDIFF_1: 23;

    end;

    theorem :: NDIFF_2:10

    for R1 be RestFunc of S, T st (R1 /. ( 0. S)) = ( 0. T) holds for R2 be RestFunc of T, U st (R2 /. ( 0. T)) = ( 0. U) holds (R2 * R1) is RestFunc of S, U

    proof

      let R1 be RestFunc of S, T such that

       A1: (R1 /. ( 0. S)) = ( 0. T);

      let R2 be RestFunc of T, U such that

       A2: (R2 /. ( 0. T)) = ( 0. U);

      R2 is total by NDIFF_1:def 5;

      then ( dom R2) = the carrier of T by PARTFUN1:def 2;

      then

       A3: ( rng R1) c= ( dom R2);

      

       A4: R1 is total by NDIFF_1:def 5;

      then

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

       A6:

      now

        consider d1 be Real such that

         A7: 0 < d1 and

         A8: for h be Point of S st ||.h.|| < d1 holds ||.(R1 /. h).|| <= (1 * ||.h.||) by A1, Th7;

        let e0 be Real such that

         A9: e0 > 0 ;

        set e = (e0 / 2);

        

         A10: e < e0 by A9, XREAL_1: 216;

        e > 0 by A9, XREAL_1: 215;

        then

        consider d2 be Real such that

         A11: 0 < d2 and

         A12: for z be Point of T st ||.z.|| < d2 holds ||.(R2 /. z).|| <= (e * ||.z.||) by A2, Th7;

        set d = ( min (d1,d2));

        

         A13: d <= d2 by XXREAL_0: 17;

        

         A14: d <= d1 by XXREAL_0: 17;

         A15:

        now

          let h be Point of S such that

           A16: h <> ( 0. S) and

           A17: ||.h.|| < d;

           ||.h.|| < d1 by A14, A17, XXREAL_0: 2;

          then

           A18: ||.(R1 /. h).|| <= (1 * ||.h.||) by A8;

          then ||.(R1 /. h).|| < d by A17, XXREAL_0: 2;

          then ||.(R1 /. h).|| < d2 by A13, XXREAL_0: 2;

          then

           A19: ||.(R2 /. (R1 /. h)).|| <= (e * ||.(R1 /. h).||) by A12;

          (e * ||.(R1 /. h).||) <= (e * ||.h.||) by A9, A18, XREAL_1: 64;

          then

           A20: ||.(R2 /. (R1 /. h)).|| <= (e * ||.h.||) by A19, XXREAL_0: 2;

          

           A21: ||.h.|| <> 0 by A16, NORMSP_0:def 5;

          then ||.h.|| > 0 by NORMSP_1: 4;

          then (( ||.h.|| " ) * ||.(R2 /. (R1 /. h)).||) <= (( ||.h.|| " ) * (e * ||.h.||)) by A20, XREAL_1: 64;

          then (( ||.h.|| " ) * ||.(R2 /. (R1 /. h)).||) <= ((( ||.h.|| " ) * ||.h.||) * e);

          then

           A22: (( ||.h.|| " ) * ||.(R2 /. (R1 /. h)).||) <= (1 * e) by A21, XCMPLX_0:def 7;

          (R2 /. (R1 /. h)) = ((R2 * R1) /. h) by A5, A3, PARTFUN2: 5;

          hence (( ||.h.|| " ) * ||.((R2 * R1) /. h).||) < e0 by A10, A22, XXREAL_0: 2;

        end;

         0 < d by A11, A7, XXREAL_0: 15;

        hence ex d be Real st d > 0 & for h be Point of S st h <> ( 0. S) & ||.h.|| < d holds (( ||.h.|| " ) * ||.((R2 * R1) /. h).||) < e0 by A15;

      end;

      ( dom (R2 * R1)) = ( dom R1) by A3, RELAT_1: 27

      .= the carrier of S by A4, PARTFUN1:def 2;

      then (R2 * R1) is total by PARTFUN1:def 2;

      hence thesis by A6, NDIFF_1: 23;

    end;

    theorem :: NDIFF_2:11

    

     Th11: for R1 be RestFunc of S, T st (R1 /. ( 0. S)) = ( 0. T) holds for R2 be RestFunc of T, U st (R2 /. ( 0. T)) = ( 0. U) holds for L be Lipschitzian LinearOperator of S, T holds (R2 * (L + R1)) is RestFunc of S, U

    proof

      let R1 be RestFunc of S, T;

      assume (R1 /. ( 0. S)) = ( 0. T);

      then

      consider d0 be Real such that

       A1: 0 < d0 and

       A2: for h be Point of S st ||.h.|| < d0 holds ||.(R1 /. h).|| <= (1 * ||.h.||) by Th7;

      let R2 be RestFunc of T, U such that

       A3: (R2 /. ( 0. T)) = ( 0. U);

      let L be Lipschitzian LinearOperator of S, T;

      consider K be Real such that

       A4: 0 <= K and

       A5: for h be Point of S holds ||.(L . h).|| <= (K * ||.h.||) by LOPBAN_1:def 8;

      R2 is total by NDIFF_1:def 5;

      then ( dom R2) = the carrier of T by PARTFUN1:def 2;

      then

       A6: ( rng (L + R1)) c= ( dom R2);

      R1 is total by NDIFF_1:def 5;

      then

       A7: (L + R1) is total by VFUNCT_1: 32;

      then

       A8: ( dom (L + R1)) = the carrier of S by PARTFUN1:def 2;

       A9:

      now

        let ee be Real such that

         A10: ee > 0 ;

        set e = (ee / 2);

        

         A11: e < ee by A10, XREAL_1: 216;

        set e1 = (e / (1 + K));

        e > 0 by A10, XREAL_1: 215;

        then ( 0 / (1 + K)) < (e / (1 + K)) by A4, XREAL_1: 74;

        then

        consider d be Real such that

         A12: 0 < d and

         A13: for z be Point of T st ||.z.|| < d holds ||.(R2 /. z).|| <= (e1 * ||.z.||) by A3, Th7;

        set d1 = (d / (1 + K));

        set dd1 = ( min (d0,d1));

        

         A14: dd1 <= d1 by XXREAL_0: 17;

        

         A15: dd1 <= d0 by XXREAL_0: 17;

         A16:

        now

          let h be Point of S such that

           A17: h <> ( 0. S) and

           A18: ||.h.|| < dd1;

           ||.h.|| < d0 by A15, A18, XXREAL_0: 2;

          then

           A19: ||.(R1 /. h).|| <= (1 * ||.h.||) by A2;

           ||.(L . h).|| <= (K * ||.h.||) by A5;

          then ||.((L . h) + (R1 /. h)).|| <= ( ||.(L . h).|| + ||.(R1 /. h).||) & ( ||.(L . h).|| + ||.(R1 /. h).||) <= ((K * ||.h.||) + (1 * ||.h.||)) by A19, NORMSP_1:def 1, XREAL_1: 7;

          then

           A20: ||.((L . h) + (R1 /. h)).|| <= ((K + 1) * ||.h.||) by XXREAL_0: 2;

           ||.h.|| < d1 by A14, A18, XXREAL_0: 2;

          then ((K + 1) * ||.h.||) < ((K + 1) * d1) by A4, XREAL_1: 68;

          then ||.((L . h) + (R1 /. h)).|| < ((K + 1) * d1) by A20, XXREAL_0: 2;

          then ||.((L . h) + (R1 /. h)).|| < d by A4, XCMPLX_1: 87;

          then

           A21: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= (e1 * ||.((L . h) + (R1 /. h)).||) by A13;

          (e1 * ||.((L . h) + (R1 /. h)).||) <= (e1 * ((K + 1) * ||.h.||)) by A4, A10, A20, XREAL_1: 64;

          then

           A22: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= (e1 * ((K + 1) * ||.h.||)) by A21, XXREAL_0: 2;

          

           A23: (R2 /. ((L . h) + (R1 /. h))) = (R2 /. ((L /. h) + (R1 /. h)))

          .= (R2 /. ((L + R1) /. h)) by A8, VFUNCT_1:def 1

          .= ((R2 * (L + R1)) /. h) by A8, A6, PARTFUN2: 5;

          

           A24: ||.h.|| <> 0 by A17, NORMSP_0:def 5;

          then ||.h.|| > 0 by NORMSP_1: 4;

          then (( ||.h.|| " ) * ||.((R2 * (L + R1)) /. h).||) <= (( ||.h.|| " ) * ((e1 * (K + 1)) * ||.h.||)) by A23, A22, XREAL_1: 64;

          then (( ||.h.|| " ) * ||.((R2 * (L + R1)) /. h).||) <= ((( ||.h.|| * ( ||.h.|| " )) * e1) * (K + 1));

          then (( ||.h.|| " ) * ||.((R2 * (L + R1)) /. h).||) <= ((1 * e1) * (K + 1)) by A24, XCMPLX_0:def 7;

          then (( ||.h.|| " ) * ||.((R2 * (L + R1)) /. h).||) <= e by A4, XCMPLX_1: 87;

          hence (( ||.h.|| " ) * ||.((R2 * (L + R1)) /. h).||) < ee by A11, XXREAL_0: 2;

        end;

        ( 0 / (1 + K)) < (d / (1 + K)) by A4, A12, XREAL_1: 74;

        then 0 < dd1 by A1, XXREAL_0: 15;

        hence ex dd1 be Real st dd1 > 0 & for h be Point of S st h <> ( 0. S) & ||.h.|| < dd1 holds (( ||.h.|| " ) * ||.((R2 * (L + R1)) /. h).||) < ee by A16;

      end;

      ( dom (R2 * (L + R1))) = ( dom (L + R1)) by A6, RELAT_1: 27

      .= the carrier of S by A7, PARTFUN1:def 2;

      then (R2 * (L + R1)) is total by PARTFUN1:def 2;

      hence thesis by A9, NDIFF_1: 23;

    end;

    theorem :: NDIFF_2:12

    

     Th12: for R1 be RestFunc of S, T st (R1 /. ( 0. S)) = ( 0. T) holds for R2 be RestFunc of T, U st (R2 /. ( 0. T)) = ( 0. U) holds for L1 be Lipschitzian LinearOperator of S, T holds for L2 be Lipschitzian LinearOperator of T, U holds ((L2 * R1) + (R2 * (L1 + R1))) is RestFunc of S, U

    proof

      let R1 be RestFunc of S, T such that

       A1: (R1 /. ( 0. S)) = ( 0. T);

      let R2 be RestFunc of T, U such that

       A2: (R2 /. ( 0. T)) = ( 0. U);

      let L1 be Lipschitzian LinearOperator of S, T;

      let L2 be Lipschitzian LinearOperator of T, U;

      

       A3: (L2 * R1) is RestFunc of S, U by Th9;

      (R2 * (L1 + R1)) is RestFunc of S, U by A1, A2, Th11;

      hence thesis by A3, NDIFF_1: 28;

    end;

    theorem :: NDIFF_2:13

    for f1 be PartFunc of S, T st f1 is_differentiable_in x0 holds for f2 be PartFunc of T, U st f2 is_differentiable_in (f1 /. x0) holds (f2 * f1) is_differentiable_in x0 & ( diff ((f2 * f1),x0)) = (( diff (f2,(f1 /. x0))) * ( diff (f1,x0)))

    proof

      let f1 be PartFunc of S, T such that

       A1: f1 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A2: N1 c= ( dom f1) and

       A3: ex R1 be RestFunc of S, T st (R1 /. ( 0. S)) = ( 0. T) & R1 is_continuous_in ( 0. S) & for x be Point of S st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((( diff (f1,x0)) . (x - x0)) + (R1 /. (x - x0))) by A1, NDIFF_1: 47;

      let f2 be PartFunc of T, U;

      assume f2 is_differentiable_in (f1 /. x0);

      then

      consider N2 be Neighbourhood of (f1 /. x0) such that

       A4: N2 c= ( dom f2) and

       A5: ex R2 be RestFunc of T, U st (R2 /. ( 0. T)) = ( 0. U) & R2 is_continuous_in ( 0. T) & for y be Point of T st y in N2 holds ((f2 /. y) - (f2 /. (f1 /. x0))) = ((( diff (f2,(f1 /. x0))) . (y - (f1 /. x0))) + (R2 /. (y - (f1 /. x0)))) by NDIFF_1: 47;

      consider R2 be RestFunc of T, U such that

       A6: (R2 /. ( 0. T)) = ( 0. U) and

       A7: for y be Point of T st y in N2 holds ((f2 /. y) - (f2 /. (f1 /. x0))) = ((( diff (f2,(f1 /. x0))) . (y - (f1 /. x0))) + (R2 /. (y - (f1 /. x0)))) by A5;

      set L2 = ( modetrans (( diff (f2,(f1 /. x0))),T,U));

      set L1 = ( modetrans (( diff (f1,x0)),S,T));

      ( 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 LB1 = ( diff (f1,x0)) as Element of ( BoundedLinearOperators (S,T));

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

      then

      reconsider LB2 = ( diff (f2,(f1 /. x0))) as Element of ( BoundedLinearOperators (T,U));

      consider R1 be RestFunc of S, T such that

       A8: (R1 /. ( 0. S)) = ( 0. T) and

       A9: for x be Point of S st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((( diff (f1,x0)) . (x - x0)) + (R1 /. (x - x0))) by A3;

      f1 is_continuous_in x0 by A1, NDIFF_1: 44;

      then

      consider N3 be Neighbourhood of x0 such that

       A10: (f1 .: N3) c= N2 by NFCONT_1: 10;

      reconsider R0 = ((L2 * R1) + (R2 * (L1 + R1))) as RestFunc of S, U by A8, A6, Th12;

      consider N be Neighbourhood of x0 such that

       A11: N c= N1 and

       A12: N c= N3 by NDIFF_1: 1;

      

       A13: N c= ( dom (f2 * f1))

      proof

        let x be object;

        assume

         A14: x in N;

        then

        reconsider x9 = x as Point of S;

        

         A15: x in N1 by A11, A14;

        then (f1 . x9) in (f1 .: N3) by A2, A12, A14, FUNCT_1:def 6;

        then (f1 . x9) in N2 by A10;

        hence thesis by A2, A4, A15, FUNCT_1: 11;

      end;

      

       A16: LB1 = ( modetrans (LB1,S,T)) & LB2 = ( modetrans (LB2,T,U)) by LOPBAN_1:def 11;

       A17:

      now

        let x be Point of S such that

         A18: x in N;

        

         A19: ((f1 /. x) - (f1 /. x0)) = ((( diff (f1,x0)) . (x - x0)) + (R1 /. (x - x0))) by A9, A11, A18;

        x in N1 by A11, A18;

        then (f1 . x) in (f1 .: N3) by A2, A12, A18, FUNCT_1:def 6;

        then

         A20: (f1 . x) in N2 by A10;

        x in N1 by A11, A18;

        then

         A21: (f1 /. x) in N2 by A2, A20, PARTFUN1:def 6;

        ( dom L1) = the carrier of S by FUNCT_2:def 1;

        then

         A22: (L2 . (L1 . (x - x0))) = ((( diff (f2,(f1 /. x0))) * ( diff (f1,x0))) . (x - x0)) by FUNCT_1: 13;

        

         A23: x0 in N by NFCONT_1: 4;

        

         A24: R1 is total by NDIFF_1:def 5;

        then

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

        ( dom L2) = the carrier of T by FUNCT_2:def 1;

        then

         A26: ( rng R1) c= ( dom L2);

        

        then

         A27: ( dom (L2 * R1)) = ( dom R1) by RELAT_1: 27

        .= the carrier of S by A24, PARTFUN1:def 2;

        

         A28: (L1 + R1) is total by A24, VFUNCT_1: 32;

        then

         A29: ( dom (L1 + R1)) = the carrier of S by PARTFUN1:def 2;

        R2 is total by NDIFF_1:def 5;

        then ( dom R2) = the carrier of T by PARTFUN1:def 2;

        then

         A30: ( rng (L1 + R1)) c= ( dom R2);

        

        then ( dom (R2 * (L1 + R1))) = ( dom (L1 + R1)) by RELAT_1: 27

        .= the carrier of S by A28, PARTFUN1:def 2;

        

        then

         A31: ( dom ((L2 * R1) + (R2 * (L1 + R1)))) = (the carrier of S /\ the carrier of S) by A27, VFUNCT_1:def 1

        .= the carrier of S;

        

         A32: (L2 . (R1 /. (x - x0))) = (L2 /. (R1 /. (x - x0)))

        .= ((L2 * R1) /. (x - x0)) by A25, A26, PARTFUN2: 5;

        

         A33: (R2 /. ((L1 . (x - x0)) + (R1 /. (x - x0)))) = (R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0))))

        .= (R2 /. ((L1 + R1) /. (x - x0))) by A29, VFUNCT_1:def 1

        .= ((R2 * (L1 + R1)) /. (x - x0)) by A29, A30, PARTFUN2: 5;

        

        thus (((f2 * f1) /. x) - ((f2 * f1) /. x0)) = ((f2 /. (f1 /. x)) - ((f2 * f1) /. x0)) by A13, A18, PARTFUN2: 3

        .= ((f2 /. (f1 /. x)) - (f2 /. (f1 /. x0))) by A13, A23, PARTFUN2: 3

        .= ((( diff (f2,(f1 /. x0))) . ((f1 /. x) - (f1 /. x0))) + (R2 /. ((f1 /. x) - (f1 /. x0)))) by A7, A21

        .= (((L2 . (L1 . (x - x0))) + (L2 . (R1 /. (x - x0)))) + ((R2 * (L1 + R1)) /. (x - x0))) by A16, A19, A33, VECTSP_1:def 20

        .= ((L2 . (L1 . (x - x0))) + (((L2 * R1) /. (x - x0)) + ((R2 * (L1 + R1)) /. (x - x0)))) by A32, RLVECT_1:def 3

        .= (((( diff (f2,(f1 /. x0))) * ( diff (f1,x0))) . (x - x0)) + (R0 /. (x - x0))) by A31, A22, VFUNCT_1:def 1;

      end;

      hence (f2 * f1) is_differentiable_in x0 by A13, NDIFF_1:def 6;

      hence thesis by A13, A17, NDIFF_1:def 7;

    end;