ckspace1.miz



    begin

    definition

      let m be non zero Element of NAT ;

      let f be PartFunc of ( REAL m), REAL ;

      let k be Nat;

      let Z be set;

      :: CKSPACE1:def1

      pred f is_continuously_differentiable_up_to_order k,Z means Z c= ( dom f) & f is_partial_differentiable_up_to_order (k,Z) & for I be non empty FinSequence of NAT st ( len I) <= k & ( rng I) c= ( Seg m) holds (f `partial| (Z,I)) is_continuous_on Z;

    end

    theorem :: CKSPACE1:1

    

     Th1: for m be non zero Element of NAT , Z be set, I be non empty FinSequence of NAT , f be PartFunc of ( REAL m), REAL st f is_partial_differentiable_on (Z,I) holds ( dom (f `partial| (Z,I))) = Z

    proof

      let m be non zero Element of NAT , Z be set, I be non empty FinSequence of NAT , f be PartFunc of ( REAL m), REAL ;

      assume

       A1: f is_partial_differentiable_on (Z,I);

      reconsider k = (( len I) - 1) as Element of NAT by INT_1: 5, FINSEQ_1: 20;

      

       A2: (f `partial| (Z,I)) = ((( PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) by PDIFF_9:def 7;

      (( PartDiffSeq (f,Z,I)) . k) is_partial_differentiable_on (Z,(I /. (k + 1))) by A1;

      hence thesis by A2, PDIFF_9:def 6;

    end;

    theorem :: CKSPACE1:2

    

     Th2: for m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL st X is open & X c= ( dom f) holds f is_continuously_differentiable_up_to_order (1,X) iff (f is_differentiable_on X & for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds for v be Element of ( REAL m) holds |.((( diff (f,x1)) . v) - (( diff (f,x0)) . v)).| <= (r * |.v.|))

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL ;

      assume

       A1: X is open & X c= ( dom f);

      hereby

        assume

         A2: f is_continuously_differentiable_up_to_order (1,X);

        now

          let i be Nat;

          assume

           A3: 1 <= i & i <= m;

          reconsider ii = i as Element of NAT by ORDINAL1:def 12;

          set I = <*ii*>;

          

           A4: ( len I) = 1 by FINSEQ_1: 40;

          i in ( Seg m) by A3;

          then {i} c= ( Seg m) by ZFMISC_1: 31;

          then

           A5: ( rng I) c= ( Seg m) by FINSEQ_1: 38;

          then

           A6: (f `partial| (X,I)) is_continuous_on X by A2, A4;

          thus f is_partial_differentiable_on (X,i) by A4, A5, A2, PDIFF_9:def 11, PDIFF_9: 81;

          hence (f `partial| (X,i)) is_continuous_on X by A1, A3, PDIFF_9: 82, A6;

        end;

        hence f is_differentiable_on X & for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds for v be Element of ( REAL m) holds |.((( diff (f,x1)) . v) - (( diff (f,x0)) . v)).| <= (r * |.v.|) by A1, PDIFF_9: 63;

      end;

      assume

       A7: f is_differentiable_on X & for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds for v be Element of ( REAL m) holds |.((( diff (f,x1)) . v) - (( diff (f,x0)) . v)).| <= (r * |.v.|);

      then

       A8: for i be Element of NAT st 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X by A1, PDIFF_9: 63;

       A9:

      now

        let I be non empty FinSequence of NAT ;

        assume

         A10: ( len I) <= 1 & ( rng I) c= ( Seg m);

        

         A11: 1 <= ( len I) by FINSEQ_1: 20;

        then 1 in ( dom I) by FINSEQ_3: 25;

        then

         A14: (I . 1) in ( rng I) by FUNCT_1: 3;

        reconsider i = (I . 1) as Element of NAT by ORDINAL1:def 12;

        

         A15: 1 <= i & i <= m by A14, A10, FINSEQ_1: 1;

        

         A16: I = <*(I . 1)*> by FINSEQ_5: 14, A10, A11, XXREAL_0: 1;

        then

         A17: I = <*i*>;

        thus f is_partial_differentiable_on (X,I) by A16, PDIFF_9: 81, A15, A8;

        (f `partial| (X,i)) is_continuous_on X by A15, A1, PDIFF_9: 63, A7;

        hence (f `partial| (X,I)) is_continuous_on X by A1, A8, A17, A15, PDIFF_9: 82;

      end;

      then for I be non empty FinSequence of NAT st ( len I) <= 1 & ( rng I) c= ( Seg m) holds f is_partial_differentiable_on (X,I);

      hence f is_continuously_differentiable_up_to_order (1,X) by A1, A9, PDIFF_9:def 11;

    end;

    theorem :: CKSPACE1:3

    

     Th3: for m be non zero Element of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL st X is open & X c= ( dom f) & f is_continuously_differentiable_up_to_order (1,X) holds f is_continuous_on X

    proof

      let m be non zero Element of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL ;

      assume

       A1: X is open & X c= ( dom f) & f is_continuously_differentiable_up_to_order (1,X);

      then

       A2: f is_differentiable_on X by Th2;

      reconsider g = ( <>* f) as PartFunc of ( REAL m), ( REAL 1);

      

       A3: g is_differentiable_on X by A1, A2, PDIFF_9: 53;

      the carrier of ( REAL-NS m) = ( REAL m) & the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider h = ( <>* f) as PartFunc of ( REAL-NS m), ( REAL-NS 1);

      h is_differentiable_on X by A3, PDIFF_6: 30;

      then h is_continuous_on X by NDIFF_1: 45;

      then g is_continuous_on X by PDIFF_7: 37;

      hence f is_continuous_on X by PDIFF_9: 44;

    end;

    theorem :: CKSPACE1:4

    

     Th4: for m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f,g be PartFunc of ( REAL m), REAL st f is_continuously_differentiable_up_to_order (k,X) & g is_continuously_differentiable_up_to_order (k,X) & X is open holds (f + g) is_continuously_differentiable_up_to_order (k,X)

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f,g be PartFunc of ( REAL m), REAL ;

      assume

       A1: f is_continuously_differentiable_up_to_order (k,X) & g is_continuously_differentiable_up_to_order (k,X) & X is open;

      

       A2: ( dom (f + g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

      for I be non empty FinSequence of NAT st ( len I) <= k & ( rng I) c= ( Seg m) holds ((f + g) `partial| (X,I)) is_continuous_on X

      proof

        let I be non empty FinSequence of NAT ;

        assume

         A3: ( len I) <= k & ( rng I) c= ( Seg m);

        

         A4: f is_partial_differentiable_on (X,I) by A3, PDIFF_9:def 11, A1;

        

         A5: g is_partial_differentiable_on (X,I) by A3, A1, PDIFF_9:def 11;

        reconsider f0 = (f `partial| (X,I)) as PartFunc of ( REAL m), REAL ;

        reconsider g0 = (g `partial| (X,I)) as PartFunc of ( REAL m), REAL ;

        

         A6: X = ( dom f0) by Th1, A3, PDIFF_9:def 11, A1;

        

         A7: X = ( dom g0) by Th1, A3, A1, PDIFF_9:def 11;

        

         A8: f0 is_continuous_on X by A3, A1;

        

         A9: g0 is_continuous_on X by A3, A1;

        (f0 + g0) is_continuous_on X by A8, A9, A6, A7, PDIFF_9: 46;

        hence ((f + g) `partial| (X,I)) is_continuous_on X by A1, A3, A4, A5, PDIFF_9: 75;

      end;

      hence thesis by A2, A1, PDIFF_9: 85, XBOOLE_1: 19;

    end;

    theorem :: CKSPACE1:5

    

     Th5: for m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), r be Real, f be PartFunc of ( REAL m), REAL st f is_continuously_differentiable_up_to_order (k,X) & X is open holds (r (#) f) is_continuously_differentiable_up_to_order (k,X)

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), r be Real, f be PartFunc of ( REAL m), REAL ;

      assume

       A1: f is_continuously_differentiable_up_to_order (k,X) & X is open;

      for I be non empty FinSequence of NAT st ( len I) <= k & ( rng I) c= ( Seg m) holds ((r (#) f) `partial| (X,I)) is_continuous_on X

      proof

        let I be non empty FinSequence of NAT ;

        assume

         A2: ( len I) <= k & ( rng I) c= ( Seg m);

        

         A3: f is_partial_differentiable_on (X,I) by A2, PDIFF_9:def 11, A1;

        reconsider f0 = (f `partial| (X,I)) as PartFunc of ( REAL m), REAL ;

        X = ( dom f0) by Th1, A2, PDIFF_9:def 11, A1;

        then (r (#) f0) is_continuous_on X by A2, A1, PDIFF_9: 47;

        hence ((r (#) f) `partial| (X,I)) is_continuous_on X by A1, A2, A3, PDIFF_9: 79;

      end;

      hence thesis by PDIFF_9: 86, A1, VALUED_1:def 5;

    end;

    theorem :: CKSPACE1:6

    for m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f,g be PartFunc of ( REAL m), REAL st f is_continuously_differentiable_up_to_order (k,X) & g is_continuously_differentiable_up_to_order (k,X) & X is open holds (f - g) is_continuously_differentiable_up_to_order (k,X)

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f,g be PartFunc of ( REAL m), REAL ;

      assume

       A1: f is_continuously_differentiable_up_to_order (k,X) & g is_continuously_differentiable_up_to_order (k,X) & X is open;

      

       A2: ( dom (f - g)) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

      for I be non empty FinSequence of NAT st ( len I) <= k & ( rng I) c= ( Seg m) holds ((f - g) `partial| (X,I)) is_continuous_on X

      proof

        let I be non empty FinSequence of NAT ;

        assume

         A3: ( len I) <= k & ( rng I) c= ( Seg m);

        

         A4: f is_partial_differentiable_on (X,I) by A3, PDIFF_9:def 11, A1;

        

         A5: g is_partial_differentiable_on (X,I) by A3, PDIFF_9:def 11, A1;

        reconsider f0 = (f `partial| (X,I)) as PartFunc of ( REAL m), REAL ;

        reconsider g0 = (g `partial| (X,I)) as PartFunc of ( REAL m), REAL ;

        

         A6: X = ( dom f0) by Th1, A3, PDIFF_9:def 11, A1;

        

         A7: X = ( dom g0) by Th1, A3, PDIFF_9:def 11, A1;

        

         A8: f0 is_continuous_on X by A1, A3;

        

         A9: g0 is_continuous_on X by A3, A1;

        (f0 - g0) is_continuous_on X by A8, A9, A6, A7, PDIFF_9: 46;

        hence ((f - g) `partial| (X,I)) is_continuous_on X by A1, A3, A4, A5, PDIFF_9: 77;

      end;

      hence thesis by A2, A1, PDIFF_9: 85, XBOOLE_1: 19;

    end;

    theorem :: CKSPACE1:7

    

     Th7: for m be non zero Element of NAT , Z be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , I,G be non empty FinSequence of NAT st f is_partial_differentiable_on (Z,G) holds (f `partial| (Z,(G ^ I))) = ((f `partial| (Z,G)) `partial| (Z,I))

    proof

      let m be non zero Element of NAT , Z be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , I,G be non empty FinSequence of NAT ;

      set g = (f `partial| (Z,G));

      reconsider Z0 = 0 as Element of NAT ;

      assume

       A1: f is_partial_differentiable_on (Z,G);

      

       A2: ( dom G) c= ( dom (G ^ I)) by FINSEQ_1: 26;

      

       A3: for i be Nat st i <= (( len G) - 1) holds ((G ^ I) /. (i + 1)) = (G /. (i + 1))

      proof

        let i be Nat;

        assume i <= (( len G) - 1);

        then 1 <= (i + 1) & (i + 1) <= ( len G) by NAT_1: 11, XREAL_1: 19;

        then

         A4: (i + 1) in ( dom G) by FINSEQ_3: 25;

        then ((G ^ I) /. (i + 1)) = ((G ^ I) . (i + 1)) by A2, PARTFUN1:def 6;

        then ((G ^ I) /. (i + 1)) = (G . (i + 1)) by A4, FINSEQ_1:def 7;

        hence ((G ^ I) /. (i + 1)) = (G /. (i + 1)) by A4, PARTFUN1:def 6;

      end;

      

       A5: ( len (G ^ I)) = (( len G) + ( len I)) by FINSEQ_1: 22;

      

       A6: for i be Nat st i <= (( len I) - 1) holds ((G ^ I) /. (( len G) + (i + 1))) = (I /. (i + 1))

      proof

        let i be Nat;

        assume i <= (( len I) - 1);

        then

         A7: (i + 1) <= ( len I) by XREAL_1: 19;

        then

         A8: (i + 1) in ( dom I) by FINSEQ_3: 25, NAT_1: 11;

        1 <= (( len G) + (i + 1)) by NAT_1: 11, XREAL_1: 38;

        then (( len G) + (i + 1)) in ( dom (G ^ I)) by FINSEQ_3: 25, A5, A7, XREAL_1: 7;

        

        hence ((G ^ I) /. (( len G) + (i + 1))) = ((G ^ I) . (( len G) + (i + 1))) by PARTFUN1:def 6

        .= (I . (i + 1)) by A8, FINSEQ_1:def 7

        .= (I /. (i + 1)) by A8, PARTFUN1:def 6;

      end;

      defpred P0[ Nat] means $1 <= (( len G) - 1) implies (( PartDiffSeq (f,Z,(G ^ I))) . $1) = (( PartDiffSeq (f,Z,G)) . $1);

      

       A9: P0[ 0 ]

      proof

        assume 0 <= (( len G) - 1);

        (( PartDiffSeq (f,Z,(G ^ I))) . 0 ) = (f | Z) by PDIFF_9:def 7;

        hence (( PartDiffSeq (f,Z,(G ^ I))) . 0 ) = (( PartDiffSeq (f,Z,G)) . 0 ) by PDIFF_9:def 7;

      end;

      

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

      proof

        let k be Nat;

        assume

         A11: P0[k];

        assume

         A12: (k + 1) <= (( len G) - 1);

        

         A13: k <= (k + 1) by NAT_1: 11;

        

        thus (( PartDiffSeq (f,Z,(G ^ I))) . (k + 1)) = ((( PartDiffSeq (f,Z,(G ^ I))) . k) `partial| (Z,((G ^ I) /. (k + 1)))) by PDIFF_9:def 7

        .= ((( PartDiffSeq (f,Z,G)) . k) `partial| (Z,(G /. (k + 1)))) by A13, A3, A11, A12, XXREAL_0: 2

        .= (( PartDiffSeq (f,Z,G)) . (k + 1)) by PDIFF_9:def 7;

      end;

      

       A14: for n be Nat holds P0[n] from NAT_1:sch 2( A9, A10);

      reconsider j = (( len G) - 1) as Element of NAT by INT_1: 5, FINSEQ_1: 20;

      

       A15: (( PartDiffSeq (f,Z,(G ^ I))) . ( len G)) = ((( PartDiffSeq (f,Z,(G ^ I))) . j) `partial| (Z,((G ^ I) /. (j + 1)))) by PDIFF_9:def 7

      .= ((( PartDiffSeq (f,Z,G)) . j) `partial| (Z,((G ^ I) /. (j + 1)))) by A14

      .= ((( PartDiffSeq (f,Z,G)) . j) `partial| (Z,(G /. (j + 1)))) by A3

      .= (( PartDiffSeq (f,Z,G)) . ( len G)) by PDIFF_9:def 7;

      defpred P[ Nat] means $1 <= (( len I) - 1) implies (( PartDiffSeq (g,Z,I)) . $1) = (( PartDiffSeq (f,Z,(G ^ I))) . (( len G) + $1));

      

       A16: P[ 0 ]

      proof

        assume 0 <= (( len I) - 1);

        (( PartDiffSeq (f,Z,(G ^ I))) . (( len G) + 0 )) = (( PartDiffSeq (f,Z,G)) . ( len G)) by A15

        .= g

        .= (g | Z) by PDIFF_9: 72, A1

        .= (( PartDiffSeq (g,Z,I)) . 0 ) by PDIFF_9:def 7;

        hence thesis;

      end;

      

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

      proof

        let k be Nat;

        assume

         A18: P[k];

        set i = (( len G) + k);

        assume

         A19: (k + 1) <= (( len I) - 1);

        

         A20: k <= (k + 1) by NAT_1: 11;

        ((G ^ I) /. (i + 1)) = ((G ^ I) /. (( len G) + (k + 1)));

        then

         A21: ((G ^ I) /. (i + 1)) = (I /. (k + 1)) by A6, A20, A19, XXREAL_0: 2;

        (( PartDiffSeq (f,Z,(G ^ I))) . (( len G) + (k + 1))) = ((( PartDiffSeq (f,Z,(G ^ I))) . i) `partial| (Z,((G ^ I) /. (i + 1)))) by PDIFF_9:def 7;

        hence thesis by A20, A19, A18, A21, PDIFF_9:def 7, XXREAL_0: 2;

      end;

      

       A22: for n be Nat holds P[n] from NAT_1:sch 2( A16, A17);

      reconsider j0 = (( len I) - 1) as Element of NAT by INT_1: 5, FINSEQ_1: 20;

      reconsider j1 = (( len (G ^ I)) - 1) as Element of NAT by INT_1: 5, FINSEQ_1: 20;

      

       A23: j1 = (( len G) + j0) by A5;

      (f `partial| (Z,(G ^ I))) = ((( PartDiffSeq (f,Z,(G ^ I))) . j1) `partial| (Z,((G ^ I) /. (j1 + 1)))) by PDIFF_9:def 7

      .= ((( PartDiffSeq (g,Z,I)) . j0) `partial| (Z,((G ^ I) /. (( len G) + (j0 + 1))))) by A22, A23

      .= ((( PartDiffSeq (g,Z,I)) . j0) `partial| (Z,(I /. (j0 + 1)))) by A6

      .= (g `partial| (Z,I)) by PDIFF_9:def 7;

      hence thesis;

    end;

    theorem :: CKSPACE1:8

    for m be non zero Element of NAT , Z be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , I,G be non empty FinSequence of NAT st f is_partial_differentiable_on (Z,G) holds (f `partial| (Z,(G ^ I))) is_continuous_on Z iff ((f `partial| (Z,G)) `partial| (Z,I)) is_continuous_on Z by Th7;

    theorem :: CKSPACE1:9

    

     Th9: for m be non zero Element of NAT , Z be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , i,j be Nat, I be non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order ((i + j),Z) & ( rng I) c= ( Seg m) & ( len I) = j holds (f `partial| (Z,I)) is_continuously_differentiable_up_to_order (i,Z)

    proof

      let m be non zero Element of NAT , Z be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , i,j be Nat, I be non empty FinSequence of NAT ;

      assume

       A1: f is_continuously_differentiable_up_to_order ((i + j),Z) & ( rng I) c= ( Seg m) & ( len I) = j;

      then

       A2: Z c= ( dom f) & f is_partial_differentiable_up_to_order ((i + j),Z) & for I be non empty FinSequence of NAT st ( len I) <= (i + j) & ( rng I) c= ( Seg m) holds (f `partial| (Z,I)) is_continuous_on Z;

      

       A3: f is_partial_differentiable_on (Z,I) by A2, A1, NAT_1: 11;

      f is_partial_differentiable_on (Z,I) by A2, A1, NAT_1: 11;

      hence Z c= ( dom (f `partial| (Z,I))) by Th1;

      thus (f `partial| (Z,I)) is_partial_differentiable_up_to_order (i,Z) by PDIFF_9: 83, A1;

      let J be non empty FinSequence of NAT ;

      assume

       A4: ( len J) <= i & ( rng J) c= ( Seg m);

      reconsider G = (I ^ J) as non empty FinSequence of NAT ;

      

       A5: ( rng G) = (( rng I) \/ ( rng J)) by FINSEQ_1: 31;

      ( len G) = (( len I) + ( len J)) by FINSEQ_1: 22;

      then ( len G) <= (i + j) & ( rng G) c= ( Seg m) by A4, A5, A1, XBOOLE_1: 8, XREAL_1: 6;

      then (f `partial| (Z,G)) is_continuous_on Z by A1;

      hence thesis by A3, Th7;

    end;

    theorem :: CKSPACE1:10

    

     Th10: for m be non zero Element of NAT , Z be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , i,j be Nat st f is_continuously_differentiable_up_to_order (i,Z) & j <= i holds f is_continuously_differentiable_up_to_order (j,Z) by PDIFF_9: 84, XXREAL_0: 2;

    theorem :: CKSPACE1:11

    

     Th11: for m be non zero Element of NAT , Z be non empty Subset of ( REAL m) st Z is open holds for k be Element of NAT , f,g be PartFunc of ( REAL m), REAL st f is_continuously_differentiable_up_to_order (k,Z) & g is_continuously_differentiable_up_to_order (k,Z) holds (f (#) g) is_continuously_differentiable_up_to_order (k,Z)

    proof

      let m be non zero Element of NAT , Z be non empty Subset of ( REAL m);

      assume

       A1: Z is open;

      defpred P[ Nat] means for f,g be PartFunc of ( REAL m), REAL st f is_continuously_differentiable_up_to_order ($1,Z) & g is_continuously_differentiable_up_to_order ($1,Z) holds (f (#) g) is_continuously_differentiable_up_to_order ($1,Z);

      set Z0 = 0 qua Nat;

      

       A2: P[ 0 ]

      proof

        let f,g be PartFunc of ( REAL m), REAL ;

        assume

         A3: f is_continuously_differentiable_up_to_order ( 0 ,Z) & g is_continuously_differentiable_up_to_order ( 0 ,Z);

        ( dom (f (#) g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        hence (f (#) g) is_continuously_differentiable_up_to_order ( 0 ,Z) by A3, XBOOLE_1: 19, FINSEQ_1: 20, PDIFF_9: 87, A1;

      end;

      

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

      proof

        let k be Nat;

        assume

         A5: P[k];

        let f,g be PartFunc of ( REAL m), REAL ;

        assume

         A6: f is_continuously_differentiable_up_to_order ((k + 1),Z) & g is_continuously_differentiable_up_to_order ((k + 1),Z);

        then

         A7: f is_continuously_differentiable_up_to_order (k,Z) & g is_continuously_differentiable_up_to_order (k,Z) by Th10, NAT_1: 11;

        ( dom (f (#) g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then

         A8: Z c= ( dom (f (#) g)) by A6, XBOOLE_1: 19;

        now

          let I be non empty FinSequence of NAT ;

          assume

           A9: ( len I) <= (k + 1) & ( rng I) c= ( Seg m);

          then

           A10: f is_partial_differentiable_on (Z,I) & g is_partial_differentiable_on (Z,I) by PDIFF_9:def 11, A6;

          

           A11: (f `partial| (Z,I)) is_continuous_on Z & (g `partial| (Z,I)) is_continuous_on Z by A9, A6;

          

           A12: 1 <= ( len I) by FINSEQ_1: 20;

          then

           A13: 1 in ( dom I) by FINSEQ_3: 25;

          then

           A14: (I /. 1) = (I . 1) by PARTFUN1:def 6;

          

           A15: (I . 1) in ( rng I) by A13, FUNCT_1: 3;

          reconsider i = (I . 1) as Element of NAT by ORDINAL1:def 12;

          

           A16: 1 <= i & i <= m by A15, A9, FINSEQ_1: 1;

          per cases ;

            suppose

             A17: 1 = ( len I);

            then

             A18: I = <*(I . 1)*> by FINSEQ_5: 14;

            

             A19: (f (#) g) is_continuously_differentiable_up_to_order (k,Z) by A5, A7;

            now

              per cases ;

                suppose

                 A20: k = 0 ;

                

                 A21: I = <*i*> by A17, FINSEQ_5: 14;

                

                 A22: f is_partial_differentiable_on (Z,i) & g is_partial_differentiable_on (Z,i) by A18, A9, PDIFF_9:def 11, A6;

                

                then

                 A23: ((f (#) g) `partial| (Z,I)) = ((f (#) g) `partial| (Z,i)) by A1, A16, A21, PDIFF_9: 68, PDIFF_9: 82

                .= (((f `partial| (Z,i)) (#) g) + (f (#) (g `partial| (Z,i)))) by A1, A22, A16, PDIFF_9: 68

                .= (((f `partial| (Z,I)) (#) g) + (f (#) (g `partial| (Z,i)))) by A1, A16, A21, A22, PDIFF_9: 82

                .= (((f `partial| (Z,I)) (#) g) + (f (#) (g `partial| (Z,I)))) by A1, A16, A21, A22, PDIFF_9: 82;

                

                 A24: Z c= ( dom (f `partial| (Z,I))) & Z c= ( dom (g `partial| (Z,I))) by A9, Th1, PDIFF_9:def 11, A6;

                

                 A25: f is_continuous_on Z by A1, Th3, A6, A20;

                g is_continuous_on Z by A1, Th3, A6, A20;

                then

                 A26: ((f `partial| (Z,I)) (#) g) is_continuous_on Z by A11, A6, A24, PDIFF_9: 48;

                

                 A27: (f (#) (g `partial| (Z,I))) is_continuous_on Z by A11, A25, A6, A24, PDIFF_9: 48;

                ( dom ((f `partial| (Z,I)) (#) g)) = (( dom (f `partial| (Z,I))) /\ ( dom g)) by VALUED_1:def 4;

                then

                 A28: Z c= ( dom ((f `partial| (Z,I)) (#) g)) by A24, A6, XBOOLE_1: 19;

                ( dom (f (#) (g `partial| (Z,I)))) = (( dom f) /\ ( dom (g `partial| (Z,I)))) by VALUED_1:def 4;

                then Z c= ( dom (f (#) (g `partial| (Z,I)))) by A24, A6, XBOOLE_1: 19;

                hence ((f (#) g) `partial| (Z,I)) is_continuous_on Z by A23, A26, A27, A28, PDIFF_9: 46;

              end;

                suppose k <> 0 ;

                hence ((f (#) g) `partial| (Z,I)) is_continuous_on Z by A19, A9, A17, NAT_1: 14;

              end;

            end;

            hence ((f (#) g) `partial| (Z,I)) is_continuous_on Z;

          end;

            suppose 1 <> ( len I);

            then 1 < ( len I) by A12, XXREAL_0: 1;

            then (1 + 1) <= ( len I) by NAT_1: 13;

            then 1 <= (( len I) - 1) by XREAL_1: 19;

            then 1 <= ( len (I /^ 1)) by A12, RFINSEQ:def 1;

            then

            reconsider J = (I /^ 1) as non empty FinSequence of NAT by FINSEQ_1: 20;

            set I1 = <*i*>;

            (( len I) - 1) <= k by A9, XREAL_1: 20;

            then

             A29: ( len J) <= k by A12, RFINSEQ:def 1;

            

             A30: I = ( <*(I /. 1)*> ^ (I /^ 1)) by FINSEQ_5: 29;

            then

             A31: ( rng I1) c= ( rng I) & ( rng J) c= ( rng I) by A14, FINSEQ_1: 29, FINSEQ_1: 30;

            then

             A32: ( rng J) c= ( Seg m) by A9;

            I = (I1 ^ J) by A14, FINSEQ_5: 29;

            then

             A33: f is_partial_differentiable_on (Z,i) & g is_partial_differentiable_on (Z,i) by PDIFF_9: 80, A10;

            then

             A34: (f (#) g) is_partial_differentiable_on (Z,i) by A1, A16, PDIFF_9: 68;

            

            then

             A35: ((f (#) g) `partial| (Z,I1)) = ((f (#) g) `partial| (Z,i)) by A1, A16, PDIFF_9: 82

            .= (((f `partial| (Z,i)) (#) g) + (f (#) (g `partial| (Z,i)))) by A33, A16, PDIFF_9: 68, A1

            .= (((f `partial| (Z,I1)) (#) g) + (f (#) (g `partial| (Z,i)))) by A1, A16, A33, PDIFF_9: 82

            .= (((f `partial| (Z,I1)) (#) g) + (f (#) (g `partial| (Z,I1)))) by A1, A16, A33, PDIFF_9: 82;

            ( len I1) = 1 & ( rng I1) c= ( Seg m) by A31, A9, FINSEQ_1: 39;

            then (f `partial| (Z,I1)) is_continuously_differentiable_up_to_order (k,Z) & (g `partial| (Z,I1)) is_continuously_differentiable_up_to_order (k,Z) by Th9, A6;

            then

             A36: ((f `partial| (Z,I1)) (#) g) is_continuously_differentiable_up_to_order (k,Z) & (f (#) (g `partial| (Z,I1))) is_continuously_differentiable_up_to_order (k,Z) by A5, A7;

            then ((f `partial| (Z,I1)) (#) g) is_partial_differentiable_on (Z,J) & (f (#) (g `partial| (Z,I1))) is_partial_differentiable_on (Z,J) by A29, A32, PDIFF_9:def 11;

            then

             A37: ((((f `partial| (Z,I1)) (#) g) + (f (#) (g `partial| (Z,I1)))) `partial| (Z,J)) = ((((f `partial| (Z,I1)) (#) g) `partial| (Z,J)) + ((f (#) (g `partial| (Z,I1))) `partial| (Z,J))) by A1, A32, PDIFF_9: 75;

            

             A38: Z c= ( dom (((f `partial| (Z,I1)) (#) g) `partial| (Z,J))) & Z c= ( dom ((f (#) (g `partial| (Z,I1))) `partial| (Z,J))) by A36, Th1, A29, A32, PDIFF_9:def 11;

            (((f `partial| (Z,I1)) (#) g) `partial| (Z,J)) is_continuous_on Z & ((f (#) (g `partial| (Z,I1))) `partial| (Z,J)) is_continuous_on Z by A36, A29, A9, XBOOLE_1: 1, A31;

            then ((((f `partial| (Z,I1)) (#) g) + (f (#) (g `partial| (Z,I1)))) `partial| (Z,J)) is_continuous_on Z by A37, A38, PDIFF_9: 46;

            hence ((f (#) g) `partial| (Z,I)) is_continuous_on Z by A30, A14, A34, A35, Th7;

          end;

        end;

        hence (f (#) g) is_continuously_differentiable_up_to_order ((k + 1),Z) by A8, PDIFF_9: 87, A1, A6;

      end;

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

      hence thesis;

    end;

    theorem :: CKSPACE1:12

    

     Th12: for m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real st X is open & f = (X --> d) holds for x be Element of ( REAL m) st x in X holds f is_differentiable_in x & ( diff (f,x)) = (( REAL m) --> 0 )

    proof

      let m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real;

      assume

       A1: X is open & f = (X --> d);

      let x be Element of ( REAL m);

      assume

       A2: x in X;

      d in REAL by XREAL_0:def 1;

      then <*d*> in (1 -tuples_on REAL ) by FINSEQ_2: 98;

      then <*d*> in ( REAL 1) by EUCLID:def 1;

      then

      reconsider rd = <*d*> as Point of ( REAL-NS 1) by REAL_NS1:def 4;

      

       A3: the carrier of ( REAL-NS m) = ( REAL m) & the carrier of ( REAL-NS 1) = ( REAL 1) by REAL_NS1:def 4;

      then

      reconsider g = ( <>* f) as PartFunc of ( REAL-NS m), ( REAL-NS 1);

      reconsider x1 = x as Point of ( REAL-NS m) by REAL_NS1:def 4;

      set ZR = ( 0. ( R_NormSpace_of_BoundedLinearOperators (( REAL-NS m),( REAL-NS 1))));

      

       A4: ( 0. ( REAL-NS 1)) = ( 0* 1) by REAL_NS1:def 4

      .= (1 |-> 0 qua Real) by EUCLID:def 4

      .= <* 0 *> by FINSEQ_2: 59;

      

       A5: ZR = (( REAL m) --> <* 0 *>) by A4, A3, LOPBAN_1: 31;

      reconsider Z = X as Subset of ( REAL-NS m) by REAL_NS1:def 4;

      

       A6: Z is open by PDIFF_9: 10, A1;

      

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

      then

       A8: ( dom ( <>* f)) = X by PDIFF_9: 3;

      

       A9: Z = ( dom g) by A7, PDIFF_9: 3;

      now

        let x be object;

        assume x in ( dom ( <>* f));

        then

         A10: x in X by A7, PDIFF_9: 3;

        then

        reconsider x1 = x as Element of ( REAL m);

        (( <>* f) . x) = <*(f . x1)*> by A7, A10, PDIFF_9: 6;

        hence (( <>* f) . x) = <*d*> by A1, A10, FUNCOP_1: 7;

      end;

      then

       A11: ( <>* f) = (X --> <*d*>) by A8, FUNCOP_1: 11;

      

       A12: ( rng g) = {rd} by A11, FUNCOP_1: 8;

      then

       A13: g is_differentiable_on Z & for x be Point of ( REAL-NS m) st x in Z holds ((g `| Z) /. x) = ZR by NDIFF_1: 33, A6, A9;

      then

       A14: g is_differentiable_in x1 by A2, NDIFF_1: 31, A6;

      

       A15: ZR = ((g `| Z) /. x1) by A12, A2, NDIFF_1: 33, A6, A9

      .= ( diff (g,x1)) by A2, NDIFF_1:def 9, A13;

      

       A16: ( <>* f) is_differentiable_in x by PDIFF_6: 2, A14;

      hence f is_differentiable_in x by PDIFF_7:def 1;

      

       A17: ( diff (( <>* f),x)) = (( REAL m) --> <* 0 *>) by A5, A15, A16, PDIFF_6: 3;

      

       A18: ( dom (( proj (1,1)) * ( diff (( <>* f),x)))) = ( REAL m) by FUNCT_2:def 1;

      now

        let y be object;

        assume

         A19: y in ( dom (( proj (1,1)) * ( diff (( <>* f),x))));

        then

        reconsider y1 = y as Element of ( REAL m);

        

        thus ((( proj (1,1)) * ( diff (( <>* f),x))) . y) = (( proj (1,1)) . (( diff (( <>* f),x)) . y1)) by A19, FUNCT_1: 12

        .= (( proj (1,1)) . <* 0 *>) by A17, FUNCOP_1: 7

        .= 0 by PDIFF_1: 1;

      end;

      then (( proj (1,1)) * ( diff (( <>* f),x))) = (( dom (( proj (1,1)) * ( diff (( <>* f),x)))) --> 0 ) by FUNCOP_1: 11;

      hence ( diff (f,x)) = (( REAL m) --> 0 ) by PDIFF_7:def 2, A18;

    end;

    theorem :: CKSPACE1:13

    

     Th13: for m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real st X is open & f = (X --> d) holds for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds for v be Element of ( REAL m) holds |.((( diff (f,x1)) . v) - (( diff (f,x0)) . v)).| <= (r * |.v.|)

    proof

      let m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real;

      assume

       A1: X is open & f = (X --> d);

      let x0 be Element of ( REAL m), r be Real;

      assume

       A2: x0 in X & 0 < r;

      take s = 1 qua Real;

      thus 0 < s;

      let x1 be Element of ( REAL m);

      assume

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

      let v be Element of ( REAL m);

      

       A4: (( diff (f,x1)) . v) = ((( REAL m) --> 0 ) . v) by A1, Th12, A3

      .= 0 qua Real by FUNCOP_1: 7;

      (( diff (f,x0)) . v) = ((( REAL m) --> 0 ) . v) by A1, Th12, A2

      .= 0 qua Real by FUNCOP_1: 7;

      hence |.((( diff (f,x1)) . v) - (( diff (f,x0)) . v)).| <= (r * |.v.|) by A4, A2, COMPLEX1: 44;

    end;

    theorem :: CKSPACE1:14

    

     Th14: for m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real st X is open & f = (X --> d) holds f is_differentiable_on X & ( dom (f `| X)) = X & for x be Element of ( REAL m) st x in X holds ((f `| X) /. x) = (( REAL m) --> 0 )

    proof

      let m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real;

      assume

       A1: X is open & f = (X --> d);

      

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

      for x be Element of ( REAL m) st x in X holds f is_differentiable_in x by Th12, A1;

      hence f is_differentiable_on X by A2, A1, PDIFF_9: 54;

      thus ( dom (f `| X)) = X by PDIFF_9:def 4, A2;

      thus for x be Element of ( REAL m) st x in X holds ((f `| X) /. x) = (( REAL m) --> 0 )

      proof

        let x be Element of ( REAL m);

        assume

         A3: x in X;

        

        thus ((f `| X) /. x) = ( diff (f,x)) by A2, PDIFF_9:def 4, A3

        .= (( REAL m) --> 0 ) by A3, Th12, A1;

      end;

    end;

    theorem :: CKSPACE1:15

    

     Th15: for m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real, i be Element of NAT st X is open & f = (X --> d) & 1 <= i & i <= m holds f is_partial_differentiable_on (X,i) & (f `partial| (X,i)) is_continuous_on X

    proof

      let m be non zero Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real, i be Element of NAT ;

      assume

       A1: X is open;

      assume

       A2: f = (X --> d);

      assume

       A3: 1 <= i & i <= m;

      

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

      

       A5: f is_differentiable_on X by Th14, A2, A1;

      for x0 be Element of ( REAL m), r be Real st x0 in X & 0 < r holds ex s be Real st 0 < s & for x1 be Element of ( REAL m) st x1 in X & |.(x1 - x0).| < s holds for v be Element of ( REAL m) holds |.((( diff (f,x1)) . v) - (( diff (f,x0)) . v)).| <= (r * |.v.|) by A2, Th13, A1;

      hence thesis by A3, A4, A1, A5, PDIFF_9: 63;

    end;

    theorem :: CKSPACE1:16

    

     Th16: for m be non zero Element of NAT , i be Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real st X is open & f = (X --> d) & 1 <= i & i <= m holds (f `partial| (X,i)) = (X --> 0 )

    proof

      let m be non zero Element of NAT , i be Element of NAT , f be PartFunc of ( REAL m), REAL , X be non empty Subset of ( REAL m), d be Real;

      assume

       A1: X is open & f = (X --> d) & 1 <= i & i <= m;

      

       A2: f is_partial_differentiable_on (X,i) by A1, Th15;

      

       A3: ( dom (f `partial| (X,i))) = X by A2, PDIFF_9:def 6;

      now

        let x be object;

        assume

         A4: x in ( dom (f `partial| (X,i)));

        then

        reconsider x1 = x as Element of ( REAL m);

        

         A5: f is_differentiable_in x1 & ( diff (f,x1)) = (( REAL m) --> 0 ) by Th12, A1, A3, A4;

        

         A6: (( reproj (i,( 0* m))) . 1) in ( REAL m) by XREAL_0:def 1, FUNCT_2: 5;

        

         A7: ( partdiff (f,x1,i)) = (( diff (f,x1)) . (( reproj (i,( 0* m))) . 1)) by PDIFF_7: 23, A5, A1

        .= 0 by A6, FUNCOP_1: 7, A5;

        

        thus ((f `partial| (X,i)) . x) = ((f `partial| (X,i)) /. x1) by A4, PARTFUN1:def 6

        .= 0 by A7, A2, A4, A3, PDIFF_9:def 6;

      end;

      hence thesis by A3, FUNCOP_1: 11;

    end;

    

     Lm1: for m be non zero Element of NAT , I be non empty FinSequence of NAT , i be Element of NAT st ( rng I) c= ( Seg m) & i <= (( len I) - 1) holds 1 <= (I /. (i + 1)) & (I /. (i + 1)) <= m

    proof

      let m be non zero Element of NAT , I be non empty FinSequence of NAT , i be Element of NAT ;

      assume

       A1: ( rng I) c= ( Seg m);

      assume

       A2: i <= (( len I) - 1);

      

       A3: ( 0 qua Real + 1) <= (i + 1) by XREAL_1: 6;

      (i + 1) <= ((( len I) - 1) + 1) by A2, XREAL_1: 6;

      then (i + 1) in ( Seg ( len I)) by A3;

      then

       A4: (i + 1) in ( dom I) by FINSEQ_1:def 3;

      then (I . (i + 1)) in ( rng I) by FUNCT_1: 3;

      then (I /. (i + 1)) in ( rng I) by A4, PARTFUN1:def 6;

      hence 1 <= (I /. (i + 1)) & (I /. (i + 1)) <= m by FINSEQ_1: 1, A1;

    end;

    

     Lm2: for m be non zero Element of NAT , I be non empty FinSequence of NAT , i be Element of NAT st ( rng I) c= ( Seg m) & 1 <= i & i <= ( len I) holds 1 <= (I /. i) & (I /. i) <= m

    proof

      let m be non zero Element of NAT , I be non empty FinSequence of NAT , i be Element of NAT ;

      assume

       A1: ( rng I) c= ( Seg m);

      assume 1 <= i & i <= ( len I);

      then i in ( Seg ( len I));

      then

       A2: i in ( dom I) by FINSEQ_1:def 3;

      then (I . i) in ( rng I) by FUNCT_1: 3;

      then (I /. i) in ( rng I) by A2, PARTFUN1:def 6;

      hence 1 <= (I /. i) & (I /. i) <= m by FINSEQ_1: 1, A1;

    end;

    theorem :: CKSPACE1:17

    

     Th17: for m be non zero Element of NAT , I be non empty FinSequence of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , d be Real st X is open & f = (X --> d) & ( rng I) c= ( Seg m) holds (( PartDiffSeq (f,X,I)) . 0 ) = (X --> d) & for i be Element of NAT st 1 <= i & i <= ( len I) holds (( PartDiffSeq (f,X,I)) . i) = (X --> 0 )

    proof

      let m be non zero Element of NAT , I be non empty FinSequence of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , d be Real;

      assume

       A1: X is open & f = (X --> d) & ( rng I) c= ( Seg m);

      

      thus

       A2: (( PartDiffSeq (f,X,I)) . 0 ) = ((X --> d) | X) by A1, PDIFF_9:def 7

      .= ((X /\ X) --> d) by FUNCOP_1: 12

      .= (X --> d);

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len I) implies (( PartDiffSeq (f,X,I)) . $1) = (X --> 0 );

      

       A3: P[ 0 ];

      

       A4: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A5: P[i];

        assume

         A6: 1 <= (i + 1) & (i + 1) <= ( len I);

        

         A7: i <= (i + 1) by NAT_1: 12;

        per cases ;

          suppose

           A8: i = 0 ;

          

           A9: 1 <= (I /. (i + 1)) & (I /. (i + 1)) <= m by Lm2, A1, A6;

          

          thus (( PartDiffSeq (f,X,I)) . (i + 1)) = ((( PartDiffSeq (f,X,I)) . i) `partial| (X,(I /. (i + 1)))) by PDIFF_9:def 7

          .= (X --> 0 ) by A8, A9, A1, A2, Th16;

        end;

          suppose

           A10: i <> 0 ;

          

           A11: 1 <= (I /. (i + 1)) & (I /. (i + 1)) <= m by Lm2, A1, A6;

          

          thus (( PartDiffSeq (f,X,I)) . (i + 1)) = ((( PartDiffSeq (f,X,I)) . i) `partial| (X,(I /. (i + 1)))) by PDIFF_9:def 7

          .= (X --> 0 ) by A10, A11, A1, Th16, A7, A5, NAT_1: 14, XXREAL_0: 2, A6;

        end;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A3, A4);

      hence thesis;

    end;

    theorem :: CKSPACE1:18

    

     Th18: for m be non zero Element of NAT , I be non empty FinSequence of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , d be Real st X is open & f = (X --> d) & ( rng I) c= ( Seg m) holds f is_partial_differentiable_on (X,I) & (f `partial| (X,I)) is_continuous_on X

    proof

      let m be non zero Element of NAT , I be non empty FinSequence of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , d be Real;

      assume

       A1: X is open & f = (X --> d) & ( rng I) c= ( Seg m);

      for i be Element of NAT st i <= (( len I) - 1) holds (( PartDiffSeq (f,X,I)) . i) is_partial_differentiable_on (X,(I /. (i + 1)))

      proof

        let i be Element of NAT ;

        assume

         A2: i <= (( len I) - 1);

        (( len I) - 1) <= (( len I) - 0 qua Real) by XREAL_1: 10;

        then

         A3: i <= ( len I) by A2, XXREAL_0: 2;

        per cases ;

          suppose i = 0 ;

          then

           A4: (( PartDiffSeq (f,X,I)) . i) = (X --> d) by A1, Th17;

          1 <= (I /. (i + 1)) & (I /. (i + 1)) <= m by Lm1, A1, A2;

          hence thesis by A4, A1, Th15;

        end;

          suppose i <> 0 ;

          then 1 <= i by NAT_1: 14;

          then

           A5: (( PartDiffSeq (f,X,I)) . i) = (X --> 0 ) by A1, A3, Th17;

          1 <= (I /. (i + 1)) & (I /. (i + 1)) <= m by Lm1, A1, A2;

          hence thesis by A5, A1, Th15;

        end;

      end;

      hence f is_partial_differentiable_on (X,I);

      reconsider k = (( len I) - 1) as Element of NAT by INT_1: 5, FINSEQ_1: 20;

      

       A6: (f `partial| (X,I)) = ((( PartDiffSeq (f,X,I)) . k) `partial| (X,(I /. (k + 1)))) by PDIFF_9:def 7;

      

       A7: (( len I) - 1) <= (( len I) - 0 qua Real) by XREAL_1: 10;

      per cases ;

        suppose k = 0 ;

        then

         A8: (( PartDiffSeq (f,X,I)) . k) = (X --> d) by A1, Th17;

        1 <= (I /. (k + 1)) & (I /. (k + 1)) <= m by A1, Lm1;

        hence (f `partial| (X,I)) is_continuous_on X by A1, A6, A8, Th15;

      end;

        suppose k <> 0 ;

        then 1 <= k by NAT_1: 14;

        then

         A9: (( PartDiffSeq (f,X,I)) . k) = (X --> 0 ) by A1, A7, Th17;

        1 <= (I /. (k + 1)) & (I /. (k + 1)) <= m by A1, Lm1;

        hence (f `partial| (X,I)) is_continuous_on X by A1, A6, A9, Th15;

      end;

    end;

    theorem :: CKSPACE1:19

    

     Th19: for m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , d be Real st X is open & f = (X --> d) holds f is_continuously_differentiable_up_to_order (k,X)

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty Subset of ( REAL m), f be PartFunc of ( REAL m), REAL , d be Real;

      assume

       A1: X is open & f = (X --> d);

      then f is_partial_differentiable_up_to_order (k,X) by Th18;

      hence thesis by A1, Th18, FUNCT_2:def 1;

    end;

    registration

      let m be non zero Element of NAT ;

      cluster open for non empty Subset of ( REAL m);

      correctness

      proof

        ( REAL m) c= ( REAL m);

        then

        reconsider X = ( REAL m) as non empty Subset of ( REAL m);

        for x be Element of ( REAL m) st x in X holds ex r be Real st r > 0 & { y where y be Element of ( REAL m) : |.(y - x).| < r } c= X

        proof

          let x be Element of ( REAL m);

          assume x in X;

          take r = 1;

          thus r > 0 ;

          now

            let z be object;

            assume z in { y where y be Element of ( REAL m) : |.(y - x).| < r };

            then ex y be Element of ( REAL m) st z = y & |.(y - x).| < r;

            hence z in X;

          end;

          hence { y where y be Element of ( REAL m) : |.(y - x).| < r } c= X;

        end;

        then X is open by PDIFF_7: 31;

        hence thesis;

      end;

    end

    begin

    definition

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m);

      :: CKSPACE1:def2

      func Ck_Functions (k,X) -> non empty Subset of ( RAlgebra X) equals { f where f be PartFunc of ( REAL m), REAL : f is_continuously_differentiable_up_to_order (k,X) & ( dom f) = X };

      correctness

      proof

        

         A1: { f where f be PartFunc of ( REAL m), REAL : f is_continuously_differentiable_up_to_order (k,X) & ( dom f) = X } c= ( Funcs (X, REAL ))

        proof

          let x be object;

          assume x in { f where f be PartFunc of ( REAL m), REAL : f is_continuously_differentiable_up_to_order (k,X) & ( dom f) = X };

          then

          consider f be PartFunc of ( REAL m), REAL such that

           A2: x = f & f is_continuously_differentiable_up_to_order (k,X) & ( dom f) = X;

          ( rng f) c= REAL ;

          then f is Function of X, REAL by A2, FUNCT_2: 2;

          hence x in ( Funcs (X, REAL )) by A2, FUNCT_2: 8;

        end;

        

         A3: (X --> 0 ) is Function of X, REAL by XREAL_0:def 1, FUNCOP_1: 45;

        ( dom (X --> 0 )) = X by FUNCT_2:def 1;

        then

        reconsider g = (X --> 0 ) as PartFunc of ( REAL m), REAL by A3, RELSET_1: 5;

        

         A4: ( dom g) = X by FUNCT_2:def 1;

        g is_continuously_differentiable_up_to_order (k,X) by Th19;

        then g in { f where f be PartFunc of ( REAL m), REAL : f is_continuously_differentiable_up_to_order (k,X) & ( dom f) = X } by A4;

        hence thesis by A1;

      end;

    end

    registration

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m);

      cluster ( Ck_Functions (k,X)) -> additively-linearly-closed multiplicatively-closed;

      coherence

      proof

        set W = ( Ck_Functions (k,X));

        set V = ( RAlgebra X);

        

         A1: ( RAlgebra X) is RealLinearSpace by C0SP1: 7;

        for v,u be Element of V st v in W & u in W holds (v + u) in W

        proof

          let v,u be Element of V such that

           A2: v in W & u in W;

          consider v1 be PartFunc of ( REAL m), REAL such that

           A3: v1 = v & v1 is_continuously_differentiable_up_to_order (k,X) & ( dom v1) = X by A2;

          consider u1 be PartFunc of ( REAL m), REAL such that

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

          

           A5: ( dom (v1 + u1)) = (( dom v1) /\ ( dom u1)) by VALUED_1:def 1;

          

           A6: (v1 + u1) is_continuously_differentiable_up_to_order (k,X) by A3, A4, Th4;

          reconsider h = (v + u) as Element of ( Funcs (X, REAL ));

          

           A7: ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL by FUNCT_2:def 2;

          

           A8: (( dom v1) /\ ( dom u1)) = (X /\ X) by A4, A3;

          for x be object st x in ( dom h) holds (h . x) = ((v1 . x) + (u1 . x)) by A3, A4, FUNCSDOM: 1;

          then (v + u) = (v1 + u1) by A8, A7, VALUED_1:def 1;

          hence (v + u) in W by A6, A3, A4, A5;

        end;

        then

         A9: W is add-closed by IDEAL_1:def 1;

        

         A10: for v be Element of V st v in W holds ( - v) in W

        proof

          let v be Element of V such that

           A11: v in W;

          consider v1 be PartFunc of ( REAL m), REAL such that

           A12: v1 = v & v1 is_continuously_differentiable_up_to_order (k,X) & ( dom v1) = X by A11;

          

           A13: ( dom ( - v1)) = X by VALUED_1:def 5, A12;

          

           A14: ( - v1) is_continuously_differentiable_up_to_order (k,X) by A12, Th5;

          reconsider h = ( - v), v2 = v as Element of ( Funcs (X, REAL ));

          

           A15: h = (( - 1) * v) by A1, RLVECT_1: 16;

          

           A16: ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL by FUNCT_2:def 2;

          now

            let x be object;

            assume x in ( dom h);

            then

            reconsider y = x as Element of X;

            (h . x) = (( - 1) * (v2 . y)) by A15, FUNCSDOM: 4;

            hence (h . x) = ( - (v1 . x)) by A12;

          end;

          then ( - v) = ( - v1) by A12, A16, VALUED_1: 9;

          hence ( - v) in W by A14, A13;

        end;

        for a be Real, u be Element of V st u in W holds (a * u) in W

        proof

          let a be Real, u be Element of V such that

           A17: u in W;

          consider u1 be PartFunc of ( REAL m), REAL such that

           A18: u1 = u & u1 is_continuously_differentiable_up_to_order (k,X) & ( dom u1) = X by A17;

          

           A19: ( dom (a (#) u1)) = X by A18, VALUED_1:def 5;

          

           A20: (a (#) u1) is_continuously_differentiable_up_to_order (k,X) by A18, Th5;

          reconsider h = (a * u) as Element of ( Funcs (X, REAL ));

          

           A21: ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL by FUNCT_2:def 2;

          for x be object st x in ( dom h) holds (h . x) = (a * (u1 . x)) by A18, FUNCSDOM: 4;

          then (a * u) = (a (#) u1) by A18, A21, VALUED_1:def 5;

          hence (a * u) in W by A20, A19;

        end;

        hence ( Ck_Functions (k,X)) is additively-linearly-closed by A9, A10, C0SP1:def 1, C0SP1:def 10;

        

         A22: for v,u be Element of V st v in W & u in W holds (v * u) in W

        proof

          let v,u be Element of V such that

           A23: v in W & u in W;

          consider v1 be PartFunc of ( REAL m), REAL such that

           A24: v1 = v & v1 is_continuously_differentiable_up_to_order (k,X) & ( dom v1) = X by A23;

          consider u1 be PartFunc of ( REAL m), REAL such that

           A25: u1 = u & u1 is_continuously_differentiable_up_to_order (k,X) & ( dom u1) = X by A23;

          

           A26: ( dom (v1 (#) u1)) = (( dom v1) /\ ( dom u1)) by VALUED_1:def 4

          .= X by A24, A25;

          

           A27: (v1 (#) u1) is_continuously_differentiable_up_to_order (k,X) by A24, A25, Th11;

          reconsider h = (v * u) as Element of ( Funcs (X, REAL ));

          

           A28: ex f be Function st h = f & ( dom f) = X & ( rng f) c= REAL by FUNCT_2:def 2;

          

           A29: (( dom v1) /\ ( dom u1)) = (X /\ X) by A25, A24;

          for x be object st x in ( dom h) holds (h . x) = ((v1 . x) * (u1 . x)) by A24, A25, FUNCSDOM: 2;

          then (v * u) = (v1 (#) u1) by A29, A28, VALUED_1:def 4;

          hence (v * u) in W by A27, A26;

        end;

        set g = ( RealFuncUnit X);

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

        then

        reconsider g as PartFunc of ( REAL m), REAL by RELSET_1: 5;

        

         A30: ( dom g) = X by FUNCT_2:def 1;

        g is_continuously_differentiable_up_to_order (k,X) by Th19;

        then ( 1. V) in W by A30;

        hence thesis by A22, C0SP1:def 4;

      end;

    end

    definition

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m);

      :: CKSPACE1:def3

      func R_Algebra_of_Ck_Functions (k,X) -> Subalgebra of ( RAlgebra X) equals AlgebraStr (# ( Ck_Functions (k,X)), ( mult_ (( Ck_Functions (k,X)),( RAlgebra X))), ( Add_ (( Ck_Functions (k,X)),( RAlgebra X))), ( Mult_ (( Ck_Functions (k,X)),( RAlgebra X))), ( One_ (( Ck_Functions (k,X)),( RAlgebra X))), ( Zero_ (( Ck_Functions (k,X)),( RAlgebra X))) #);

      coherence by C0SP1: 6;

    end

    registration

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m);

      cluster ( R_Algebra_of_Ck_Functions (k,X)) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital commutative associative right_unital right-distributive scalar-associative vector-associative;

      coherence

      proof

        now

          let v be VECTOR of ( R_Algebra_of_Ck_Functions (k,X));

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

          (1 * v) = (1 * v1) by C0SP1: 8;

          hence (1 * v) = v by FUNCSDOM: 12;

        end;

        hence thesis;

      end;

    end

    theorem :: CKSPACE1:20

    for m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m), F,G,H be VECTOR of ( R_Algebra_of_Ck_Functions (k,X)), f,g,h be PartFunc of ( REAL m), REAL holds (f = F & g = G & h = H implies (H = (F + G) iff (for x be Element of X holds (h . x) = ((f . x) + (g . x)))))

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m);

      let F,G,H be VECTOR of ( R_Algebra_of_Ck_Functions (k,X));

      let f,g,h be PartFunc of ( REAL m), REAL ;

      assume

       A1: f = F & g = G & h = H;

      reconsider f1 = F, g1 = G, h1 = H as VECTOR of ( RAlgebra X) by TARSKI:def 3;

      hereby

        assume

         A2: H = (F + G);

        let x be Element of X;

        h1 = (f1 + g1) by A2, C0SP1: 8;

        hence (h . x) = ((f . x) + (g . x)) by A1, FUNCSDOM: 1;

      end;

      assume for x be Element of X holds (h . x) = ((f . x) + (g . x));

      then h1 = (f1 + g1) by A1, FUNCSDOM: 1;

      hence H = (F + G) by C0SP1: 8;

    end;

    theorem :: CKSPACE1:21

    for m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m), F,G,H be VECTOR of ( R_Algebra_of_Ck_Functions (k,X)), f,g,h be PartFunc of ( REAL m), REAL , a be Real holds (f = F & g = G implies (G = (a * F) iff for x be Element of X holds (g . x) = (a * (f . x))))

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m), F,G,H be VECTOR of ( R_Algebra_of_Ck_Functions (k,X)), f,g,h be PartFunc of ( REAL m), REAL , a be Real;

      assume

       A1: f = F & g = G;

      reconsider f1 = F, g1 = G as VECTOR of ( RAlgebra X) by TARSKI:def 3;

      hereby

        assume

         A2: G = (a * F);

        let x be Element of X;

        g1 = (a * f1) by A2, C0SP1: 8;

        hence (g . x) = (a * (f . x)) by A1, FUNCSDOM: 4;

      end;

      assume for x be Element of X holds (g . x) = (a * (f . x));

      then g1 = (a * f1) by A1, FUNCSDOM: 4;

      hence G = (a * F) by C0SP1: 8;

    end;

    theorem :: CKSPACE1:22

    for m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m), F,G,H be VECTOR of ( R_Algebra_of_Ck_Functions (k,X)), f,g,h be PartFunc of ( REAL m), REAL holds (f = F & g = G & h = H implies (H = (F * G) iff (for x be Element of X holds (h . x) = ((f . x) * (g . x)))))

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m), F,G,H be VECTOR of ( R_Algebra_of_Ck_Functions (k,X)), f,g,h be PartFunc of ( REAL m), REAL ;

      assume

       A1: f = F & g = G & h = H;

      reconsider f1 = F, g1 = G, h1 = H as VECTOR of ( RAlgebra X) by TARSKI:def 3;

      hereby

        assume

         A2: H = (F * G);

        let x be Element of X;

        h1 = (f1 * g1) by A2, C0SP1: 8;

        hence (h . x) = ((f . x) * (g . x)) by A1, FUNCSDOM: 2;

      end;

      assume for x be Element of X holds (h . x) = ((f . x) * (g . x));

      then h1 = (f1 * g1) by A1, FUNCSDOM: 2;

      hence H = (F * G) by C0SP1: 8;

    end;

    theorem :: CKSPACE1:23

    for m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m) holds ( 0. ( R_Algebra_of_Ck_Functions (k,X))) = (X --> 0 )

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m);

      ( 0. ( RAlgebra X)) = (X --> 0 );

      hence thesis by C0SP1: 8;

    end;

    theorem :: CKSPACE1:24

    for m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m) holds ( 1_ ( R_Algebra_of_Ck_Functions (k,X))) = (X --> 1)

    proof

      let m be non zero Element of NAT , k be Element of NAT , X be non empty open Subset of ( REAL m);

      ( 1_ ( RAlgebra X)) = (X --> 1);

      hence thesis by C0SP1: 8;

    end;