vsdiff_1.miz



    begin

    reserve C for non empty set;

    reserve GF for Field,

V for VectSp of GF,

v,u for Element of V,

W for Subset of V;

    reserve f,f1,f2,f3 for PartFunc of C, V;

    definition

      let C;

      let GF, V;

      let f be PartFunc of C, V;

      let r be Element of GF;

      deffunc F( Element of C) = (r * (f /. $1));

      defpred P[ set] means $1 in ( dom f);

      :: VSDIFF_1:def1

      func r (#) f -> PartFunc of C, V means

      : Def4X: ( dom it ) = ( dom f) & for c be Element of C st c in ( dom it ) holds (it /. c) = (r * (f /. c));

      existence

      proof

        consider F be PartFunc of C, V such that

         A1: for c be Element of C holds c in ( dom F) iff P[c] and

         A2: for c be Element of C st c in ( dom F) holds (F /. c) = F(c) from PARTFUN2:sch 2;

        take F;

        thus thesis by A1, A2, SUBSET_1: 3;

      end;

      uniqueness

      proof

        set X = ( dom f);

        thus for f,g be PartFunc of C, V st (( dom f) = X & for c be Element of C st c in ( dom f) holds (f /. c) = F(c)) & (( dom g) = X & for c be Element of C st c in ( dom g) holds (g /. c) = F(c)) holds f = g from PARTFUN2:sch 3;

      end;

    end

    registration

      let C, GF, V;

      let f be Function of C, V;

      let r be Element of GF;

      cluster (r (#) f) -> total;

      coherence

      proof

        ( dom (r (#) f)) = ( dom f) by Def4X

        .= C by FUNCT_2:def 1;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    definition

      let GF, V, v, W;

      :: VSDIFF_1:def2

      func v ++ W -> Subset of V equals { (v + u) : u in W };

      coherence

      proof

        set Y = { (v + u) : u in W };

        defpred Sep[ object] means ex u st $1 = (v + u) & u in W;

        consider X be set such that

         A1: for x be object holds x in X iff x in the carrier of V & Sep[x] from XBOOLE_0:sch 1;

        for x be object st x in X holds x in the carrier of V by A1;

        then

        reconsider X as Subset of V by TARSKI:def 3;

        

         A2: Y c= X

        proof

          let x be object;

          assume x in Y;

          then ex u st x = (v + u) & u in W;

          hence thesis by A1;

        end;

        X c= Y

        proof

          let x be object;

          assume x in X;

          then ex u st x = (v + u) & u in W by A1;

          hence thesis;

        end;

        hence thesis by A2, XBOOLE_0:def 10;

      end;

    end

    definition

      let F,G be Field;

      let V be VectSp of F;

      let W be VectSp of G;

      let f be PartFunc of V, W;

      let h be Element of V;

      :: VSDIFF_1:def3

      func Shift (f,h) -> PartFunc of V, W means

      : Def1: ( dom it ) = (( - h) ++ ( dom f)) & (for x be Element of V st x in (( - h) ++ ( dom f)) holds (it . x) = (f . (x + h)));

      existence

      proof

        deffunc F( Element of V) = ( In ((f . ($1 + h)),the carrier of W));

        set X = (( - h) ++ ( dom f));

        defpred P[ set] means $1 in X;

        consider F be PartFunc of V, W such that

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

        take F;

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

        then

         A2: X c= ( dom F) by TARSKI:def 3;

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

        then ( dom F) c= X by TARSKI:def 3;

        hence ( dom F) = X by A2, XBOOLE_0:def 10;

        for x be Element of V st x in X holds (F . x) = (f . (x + h))

        proof

          let x be Element of V;

          assume

           A3: x in X;

          then

           A4: (F . x) = F(x) by A1;

          consider u be Element of V such that

           A5: x = (( - h) + u) & u in ( dom f) by A3;

          (x + h) = (u + (( - h) + h)) by RLVECT_1:def 3, A5

          .= (u + ( 0. V)) by VECTSP_1: 16

          .= u by RLVECT_1:def 4;

          hence thesis by A4, SUBSET_1:def 8, PARTFUN1: 4, A5;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be PartFunc of V, W;

        set X = (( - h) ++ ( dom f));

        assume that

         A6: ( dom f1) = X and

         A7: for x be Element of V st x in X holds (f1 . x) = (f . (x + h)) and

         A8: ( dom f2) = X and

         A9: for x be Element of V st x in X holds (f2 . x) = (f . (x + h));

        for x be Element of V st x in ( dom f1) holds (f1 . x) = (f2 . x)

        proof

          let x be Element of V;

          assume

           A10: x in ( dom f1);

          then (f1 . x) = (f . (x + h)) by A6, A7;

          hence thesis by A6, A9, A10;

        end;

        hence f1 = f2 by A6, A8, PARTFUN1: 5;

      end;

    end

    theorem :: VSDIFF_1:1

    

     MEASURE624: for x be Element of V, A be Subset of V st A = the carrier of V holds (x ++ A) = A

    proof

      let x be Element of V, A be Subset of V;

      assume

       P0: A = the carrier of V;

      for y be object holds y in (x ++ A) iff y in A

      proof

        let y be object;

        y in A implies y in (x ++ A)

        proof

          assume y in A;

          then

          reconsider w = y as Element of V;

          ((w - x) + x) = (w - (x - x)) by RLVECT_1: 29

          .= (w - ( 0. V)) by RLVECT_1: 15

          .= w by RLVECT_1: 13;

          hence y in (x ++ A) by P0;

        end;

        hence thesis by P0;

      end;

      hence (x ++ A) = A by TARSKI: 2;

    end;

    definition

      let F,G be Field;

      let V be VectSp of F;

      let W be VectSp of G;

      let f be Function of V, W;

      let h be Element of V;

      :: original: Shift

      redefine

      :: VSDIFF_1:def4

      func Shift (f,h) -> Function of V, W means

      : Def2: for x be Element of V holds (it . x) = (f . (x + h));

      coherence

      proof

        ( dom ( Shift (f,h))) = (( - h) ++ ( dom f)) & ( dom f) = the carrier of V by Def1, FUNCT_2:def 1;

        then ( dom ( Shift (f,h))) = the carrier of V by MEASURE624;

        hence thesis by FUNCT_2:def 1;

      end;

      compatibility

      proof

        for IT be Function of V, W holds IT = ( Shift (f,h)) iff for x be Element of V holds (IT . x) = (f . (x + h))

        proof

          let IT be Function of V, W;

          hereby

            assume

             A1: IT = ( Shift (f,h));

            let x be Element of V;

            ( dom ( Shift (f,h))) = the carrier of V by A1, FUNCT_2:def 1;

            then x in ( dom ( Shift (f,h)));

            then x in (( - h) ++ ( dom f)) by Def1;

            hence (IT . x) = (f . (x + h)) by A1, Def1;

          end;

          ( dom ( Shift (f,h))) = (( - h) ++ ( dom f)) & ( dom f) = the carrier of V by Def1, FUNCT_2:def 1;

          then ( dom ( Shift (f,h))) = the carrier of V by MEASURE624;

          then

           A2: ( dom IT) = ( dom ( Shift (f,h))) by FUNCT_2:def 1;

          assume

           A3: for x be Element of V holds (IT . x) = (f . (x + h));

          for x be Element of V st x in ( dom IT) holds (IT . x) = (( Shift (f,h)) . x)

          proof

            let x be Element of V;

            assume x in ( dom IT);

            then

             A4: x in (( - h) ++ ( dom f)) by A2, Def1;

            (IT . x) = (f . (x + h)) by A3;

            hence thesis by A4, Def1;

          end;

          hence thesis by A2, PARTFUN1: 5;

        end;

        hence thesis;

      end;

    end

    definition

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be PartFunc of V, W;

      :: VSDIFF_1:def5

      func fD (f,h) -> PartFunc of V, W equals (( Shift (f,h)) - f);

      coherence ;

    end

    registration

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      cluster ( fD (f,h)) -> quasi_total;

      coherence

      proof

        ( dom ( fD (f,h))) = (( dom ( Shift (f,h))) /\ ( dom f)) by VFUNCT_1:def 2

        .= (the carrier of V /\ ( dom f)) by FUNCT_2:def 1

        .= (the carrier of V /\ the carrier of V) by FUNCT_2:def 1

        .= the carrier of V;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    definition

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be PartFunc of V, W;

      :: VSDIFF_1:def6

      func bD (f,h) -> PartFunc of V, W equals (f - ( Shift (f,( - h))));

      coherence ;

    end

    registration

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      cluster ( bD (f,h)) -> quasi_total;

      coherence

      proof

        ( dom ( bD (f,h))) = (( dom ( Shift (f,( - h)))) /\ ( dom f)) by VFUNCT_1:def 2

        .= (the carrier of V /\ ( dom f)) by FUNCT_2:def 1

        .= (the carrier of V /\ the carrier of V) by FUNCT_2:def 1

        .= the carrier of V;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    definition

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be PartFunc of V, W;

      :: VSDIFF_1:def7

      func cD (f,h) -> PartFunc of V, W equals (( Shift (f,(((2 * ( 1. F)) " ) * h))) - ( Shift (f,( - (((2 * ( 1. F)) " ) * h)))));

      coherence ;

    end

    registration

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      cluster ( cD (f,h)) -> quasi_total;

      coherence

      proof

        ( dom ( cD (f,h))) = (( dom ( Shift (f,(((2 * ( 1. F)) " ) * h)))) /\ ( dom ( Shift (f,( - (((2 * ( 1. F)) " ) * h)))))) by VFUNCT_1:def 2

        .= (the carrier of V /\ ( dom ( Shift (f,( - (((2 * ( 1. F)) " ) * h)))))) by FUNCT_2:def 1

        .= (the carrier of V /\ the carrier of V) by FUNCT_2:def 1

        .= the carrier of V;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    definition

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      :: VSDIFF_1:def8

      func forward_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means

      : Def6: (it . 0 ) = f & for n be Nat holds (it . (n + 1)) = ( fD ((it . n),h));

      existence

      proof

        reconsider fZ = f as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

        defpred R[ set, set, set] means ex g be PartFunc of V, W st $2 = g & $3 = ( fD (g,h));

        

         A1: for n be Nat holds for x be Element of ( PFuncs (the carrier of V,the carrier of W)) holds ex y be Element of ( PFuncs (the carrier of V,the carrier of W)) st R[n, x, y]

        proof

          let n be Nat;

          let x be Element of ( PFuncs (the carrier of V,the carrier of W));

          reconsider x9 = x as PartFunc of the carrier of V, the carrier of W by PARTFUN1: 46;

          reconsider y = ( fD (x9,h)) as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

          ex w be PartFunc of the carrier of V, the carrier of W st x = w & y = ( fD (w,h));

          hence thesis;

        end;

        consider g be sequence of ( PFuncs (the carrier of V,the carrier of W)) such that

         A2: (g . 0 ) = fZ & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 2( A1);

        reconsider g as Functional_Sequence of the carrier of V, the carrier of W;

        take g;

        thus (g . 0 ) = f by A2;

        let i be Nat;

         R[i, (g . i), (g . (i + 1))] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Functional_Sequence of the carrier of V, the carrier of W;

        assume that

         A3: (seq1 . 0 ) = f and

         A4: for n be Nat holds (seq1 . (n + 1)) = ( fD ((seq1 . n),h)) and

         A5: (seq2 . 0 ) = f and

         A6: for n be Nat holds (seq2 . (n + 1)) = ( fD ((seq2 . n),h));

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

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

        proof

          let k be Nat;

          assume

           A8: P[k];

          

          thus (seq1 . (k + 1)) = ( fD ((seq1 . k),h)) by A4

          .= (seq2 . (k + 1)) by A6, A8;

        end;

        

         A9: P[ 0 ] by A3, A5;

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

        then for n be Element of NAT holds P[n];

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    notation

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      synonym fdif (f,h) for forward_difference (f,h);

    end

    reserve F,G for Field,

V for VectSp of F,

W for VectSp of G;

    reserve f,f1,f2 for Function of V, W;

    reserve x,h for Element of V;

    reserve r,r1,r2 for Element of G;

    theorem :: VSDIFF_1:2

    

     Th01: for f be PartFunc of V, W st x in ( dom f) & (x + h) in ( dom f) holds (( fD (f,h)) /. x) = ((f /. (x + h)) - (f /. x))

    proof

      let f be PartFunc of V, W;

      assume

       A1: x in ( dom f) & (x + h) in ( dom f);

      

       A2: ( dom ( Shift (f,h))) = (( - h) ++ ( dom f)) by Def1;

      (( - h) + (x + h)) = (x + (h + ( - h))) by RLVECT_1:def 3

      .= (x + ( 0. V)) by VECTSP_1: 16

      .= x by RLVECT_1:def 4;

      then

       A4: x in (( - h) ++ ( dom f)) by A1;

      

       A5: (( Shift (f,h)) /. x) = (( Shift (f,h)) . x) by A2, A4, PARTFUN1:def 6

      .= (f . (x + h)) by Def1, A4

      .= (f /. (x + h)) by A1, PARTFUN1:def 6;

      x in (( dom ( Shift (f,h))) /\ ( dom f)) by A4, A2, A1, XBOOLE_0:def 4;

      then x in ( dom ( fD (f,h))) by VFUNCT_1:def 2;

      hence (( fD (f,h)) /. x) = ((f /. (x + h)) - (f /. x)) by A5, VFUNCT_1:def 2;

    end;

    theorem :: VSDIFF_1:3

    

     Th2: for n be Nat holds (( fdif (f,h)) . n) is Function of V, W

    proof

      defpred X[ Nat] means (( fdif (f,h)) . $1) is Function of V, W;

      

       A1: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        assume (( fdif (f,h)) . k) is Function of V, W;

        then ( fD ((( fdif (f,h)) . k),h)) is Function of V, W;

        hence thesis by Def6;

      end;

      

       A2: X[ 0 ] by Def6;

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

      hence thesis;

    end;

    theorem :: VSDIFF_1:4

    

     Th3: (( fD (f,h)) /. x) = ((f /. (x + h)) - (f /. x))

    proof

      ( dom f) = the carrier of V by FUNCT_2:def 1;

      hence (( fD (f,h)) /. x) = ((f /. (x + h)) - (f /. x)) by Th01;

    end;

    theorem :: VSDIFF_1:5

    

     Th4: (( bD (f,h)) /. x) = ((f /. x) - (f /. (x - h)))

    proof

      

       P1: ( dom f) = the carrier of V by FUNCT_2:def 1;

      ( dom ( Shift (f,( - h)))) = the carrier of V by FUNCT_2:def 1;

      then x in (( dom f) /\ ( dom ( Shift (f,( - h))))) by P1;

      then

       P2: x in ( dom (f - ( Shift (f,( - h))))) by VFUNCT_1:def 2;

      

      thus (( bD (f,h)) /. x) = ((f /. x) - (( Shift (f,( - h))) /. x)) by P2, VFUNCT_1:def 2

      .= ((f /. x) - (f /. (x - h))) by Def2;

    end;

    theorem :: VSDIFF_1:6

    

     Th5: (( cD (f,h)) /. x) = ((f /. (x + (((2 * ( 1. F)) " ) * h))) - (f /. (x - (((2 * ( 1. F)) " ) * h))))

    proof

      ( dom (( Shift (f,(((2 * ( 1. F)) " ) * h))) - ( Shift (f,( - (((2 * ( 1. F)) " ) * h)))))) = the carrier of V by FUNCT_2:def 1;

      

      hence (( cD (f,h)) /. x) = ((( Shift (f,(((2 * ( 1. F)) " ) * h))) /. x) - (( Shift (f,( - (((2 * ( 1. F)) " ) * h)))) /. x)) by VFUNCT_1:def 2

      .= ((f /. (x + (((2 * ( 1. F)) " ) * h))) - (( Shift (f,( - (((2 * ( 1. F)) " ) * h)))) /. x)) by Def2

      .= ((f /. (x + (((2 * ( 1. F)) " ) * h))) - (f /. (x - (((2 * ( 1. F)) " ) * h)))) by Def2;

    end;

    reserve n,m,k for Nat;

    theorem :: VSDIFF_1:7

    f is constant implies for x holds ((( fdif (f,h)) . (n + 1)) /. x) = ( 0. W)

    proof

      assume

       A1: f is constant;

      

       A2: for x holds ((f /. (x + h)) - (f /. x)) = ( 0. W)

      proof

        let x;

        (x + h) in the carrier of V;

        then

         A3: (x + h) in ( dom f) by FUNCT_2:def 1;

        x in the carrier of V;

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

        then (f /. x) = (f /. (x + h)) by A1, A3, FUNCT_1:def 10;

        hence thesis by RLVECT_1: 15;

      end;

      for x holds ((( fdif (f,h)) . (n + 1)) /. x) = ( 0. W)

      proof

        defpred X[ Nat] means for x holds ((( fdif (f,h)) . ($1 + 1)) /. x) = ( 0. W);

        

         A4: for k st X[k] holds X[(k + 1)]

        proof

          let k;

          assume

           A5: for x holds ((( fdif (f,h)) . (k + 1)) /. x) = ( 0. W);

          let x;

          

           A6: ((( fdif (f,h)) . (k + 1)) /. (x + h)) = ( 0. W) by A5;

          reconsider fdk = (( fdif (f,h)) . (k + 1)) as Function of V, W by Th2;

          ((( fdif (f,h)) . (k + 2)) /. x) = ((( fdif (f,h)) . ((k + 1) + 1)) /. x)

          .= (( fD ((( fdif (f,h)) . (k + 1)),h)) /. x) by Def6

          .= ((fdk /. (x + h)) - (fdk /. x)) by Th3

          .= (( 0. W) - ( 0. W)) by A5, A6

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

          hence thesis;

        end;

        

         A8: X[ 0 ]

        proof

          let x;

          

          thus ((( fdif (f,h)) . ( 0 + 1)) /. x) = (( fD ((( fdif (f,h)) . 0 ),h)) /. x) by Def6

          .= (( fD (f,h)) /. x) by Def6

          .= ((f /. (x + h)) - (f /. x)) by Th3

          .= ( 0. W) by A2;

        end;

        for n holds X[n] from NAT_1:sch 2( A8, A4);

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: VSDIFF_1:8

    

     Th7: ((( fdif ((r (#) f),h)) . (n + 1)) /. x) = (r * ((( fdif (f,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( fdif ((r (#) f),h)) . ($1 + 1)) /. x) = (r * ((( fdif (f,h)) . ($1 + 1)) /. x));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( fdif ((r (#) f),h)) . (k + 1)) /. x) = (r * ((( fdif (f,h)) . (k + 1)) /. x));

        let x;

        

         A3: ((( fdif ((r (#) f),h)) . (k + 1)) /. x) = (r * ((( fdif (f,h)) . (k + 1)) /. x)) & ((( fdif ((r (#) f),h)) . (k + 1)) /. (x + h)) = (r * ((( fdif (f,h)) . (k + 1)) /. (x + h))) by A2;

        reconsider rfdk = (( fdif ((r (#) f),h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fdk = (( fdif (f,h)) . (k + 1)) as Function of V, W by Th2;

        ((( fdif ((r (#) f),h)) . ((k + 1) + 1)) /. x) = (( fD ((( fdif ((r (#) f),h)) . (k + 1)),h)) /. x) by Def6

        .= ((rfdk /. (x + h)) - (rfdk /. x)) by Th3

        .= (r * ((fdk /. (x + h)) - (fdk /. x))) by VECTSP_1: 23, A3

        .= (r * (( fD (fdk,h)) /. x)) by Th3

        .= (r * ((( fdif (f,h)) . ((k + 1) + 1)) /. x)) by Def6;

        hence thesis;

      end;

      

       A6: X[ 0 ]

      proof

        let x;

        x in the carrier of V;

        then

         A7: x in ( dom (r (#) f)) by FUNCT_2:def 1;

        (x + h) in the carrier of V;

        then

         A8: (x + h) in ( dom (r (#) f)) by FUNCT_2:def 1;

        ((( fdif ((r (#) f),h)) . ( 0 + 1)) /. x) = (( fD ((( fdif ((r (#) f),h)) . 0 ),h)) /. x) by Def6

        .= (( fD ((r (#) f),h)) /. x) by Def6

        .= (((r (#) f) /. (x + h)) - ((r (#) f) /. x)) by Th3

        .= ((r * (f /. (x + h))) - ((r (#) f) /. x)) by A8, Def4X

        .= ((r * (f /. (x + h))) - (r * (f /. x))) by A7, Def4X

        .= (r * ((f /. (x + h)) - (f /. x))) by VECTSP_1: 23

        .= (r * (( fD (f,h)) /. x)) by Th3

        .= (r * (( fD ((( fdif (f,h)) . 0 ),h)) /. x)) by Def6

        .= (r * ((( fdif (f,h)) . ( 0 + 1)) /. x)) by Def6;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:9

    

     Th8: ((( fdif ((f1 + f2),h)) . (n + 1)) /. x) = (((( fdif (f1,h)) . (n + 1)) /. x) + ((( fdif (f2,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( fdif ((f1 + f2),h)) . ($1 + 1)) /. x) = (((( fdif (f1,h)) . ($1 + 1)) /. x) + ((( fdif (f2,h)) . ($1 + 1)) /. x));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( fdif ((f1 + f2),h)) . (k + 1)) /. x) = (((( fdif (f1,h)) . (k + 1)) /. x) + ((( fdif (f2,h)) . (k + 1)) /. x));

        let x;

        

         A3: ((( fdif ((f1 + f2),h)) . (k + 1)) /. x) = (((( fdif (f1,h)) . (k + 1)) /. x) + ((( fdif (f2,h)) . (k + 1)) /. x)) & ((( fdif ((f1 + f2),h)) . (k + 1)) /. (x + h)) = (((( fdif (f1,h)) . (k + 1)) /. (x + h)) + ((( fdif (f2,h)) . (k + 1)) /. (x + h))) by A2;

        reconsider fdiff12 = (( fdif ((f1 + f2),h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fdiff2 = (( fdif (f2,h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fdiff1 = (( fdif (f1,h)) . (k + 1)) as Function of V, W by Th2;

        

         A6: (( fD ((( fdif (f1,h)) . (k + 1)),h)) /. x) = (( fD (fdiff1,h)) /. x)

        .= (((( fdif (f1,h)) . (k + 1)) /. (x + h)) - ((( fdif (f1,h)) . (k + 1)) /. x)) by Th3;

        

         A7: (( fD ((( fdif (f2,h)) . (k + 1)),h)) /. x) = (( fD (fdiff2,h)) /. x)

        .= (((( fdif (f2,h)) . (k + 1)) /. (x + h)) - ((( fdif (f2,h)) . (k + 1)) /. x)) by Th3;

        ((( fdif ((f1 + f2),h)) . ((k + 1) + 1)) /. x) = (( fD ((( fdif ((f1 + f2),h)) . (k + 1)),h)) /. x) by Def6

        .= ((fdiff12 /. (x + h)) - (fdiff12 /. x)) by Th3

        .= (((((( fdif (f1,h)) . (k + 1)) /. (x + h)) + ((( fdif (f2,h)) . (k + 1)) /. (x + h))) - ((( fdif (f2,h)) . (k + 1)) /. x)) - ((( fdif (f1,h)) . (k + 1)) /. x)) by RLVECT_1: 27, A3

        .= ((((( fdif (f1,h)) . (k + 1)) /. (x + h)) + (((( fdif (f2,h)) . (k + 1)) /. (x + h)) - ((( fdif (f2,h)) . (k + 1)) /. x))) - ((( fdif (f1,h)) . (k + 1)) /. x)) by RLVECT_1: 28

        .= ((((( fdif (f2,h)) . (k + 1)) /. (x + h)) - ((( fdif (f2,h)) . (k + 1)) /. x)) + (((( fdif (f1,h)) . (k + 1)) /. (x + h)) - ((( fdif (f1,h)) . (k + 1)) /. x))) by RLVECT_1: 28

        .= (((( fdif (f1,h)) . ((k + 1) + 1)) /. x) + (( fD ((( fdif (f2,h)) . (k + 1)),h)) /. x)) by Def6, A6, A7

        .= (((( fdif (f1,h)) . ((k + 1) + 1)) /. x) + ((( fdif (f2,h)) . ((k + 1) + 1)) /. x)) by Def6;

        hence thesis;

      end;

      

       B1: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 1

      .= (the carrier of V /\ ( dom f2)) by FUNCT_2:def 1

      .= (the carrier of V /\ the carrier of V) by FUNCT_2:def 1

      .= the carrier of V;

      

       A7: X[ 0 ]

      proof

        let x;

        ((( fdif ((f1 + f2),h)) . ( 0 + 1)) /. x) = (( fD ((( fdif ((f1 + f2),h)) . 0 ),h)) /. x) by Def6

        .= (( fD ((f1 + f2),h)) /. x) by Def6

        .= (((f1 + f2) /. (x + h)) - ((f1 + f2) /. x)) by Th3

        .= (((f1 /. (x + h)) + (f2 /. (x + h))) - ((f1 + f2) /. x)) by B1, VFUNCT_1:def 1

        .= (((f1 /. (x + h)) + (f2 /. (x + h))) - ((f1 /. x) + (f2 /. x))) by B1, VFUNCT_1:def 1

        .= ((((f1 /. (x + h)) + (f2 /. (x + h))) - (f2 /. x)) - (f1 /. x)) by RLVECT_1: 27

        .= (((f1 /. (x + h)) + ((f2 /. (x + h)) - (f2 /. x))) - (f1 /. x)) by RLVECT_1: 28

        .= (((f2 /. (x + h)) - (f2 /. x)) + ((f1 /. (x + h)) - (f1 /. x))) by RLVECT_1: 28

        .= ((( fD (f1,h)) /. x) + ((f2 /. (x + h)) - (f2 /. x))) by Th3

        .= ((( fD (f1,h)) /. x) + (( fD (f2,h)) /. x)) by Th3

        .= ((( fD ((( fdif (f1,h)) . 0 ),h)) /. x) + (( fD (f2,h)) /. x)) by Def6

        .= ((( fD ((( fdif (f1,h)) . 0 ),h)) /. x) + (( fD ((( fdif (f2,h)) . 0 ),h)) /. x)) by Def6

        .= (((( fdif (f1,h)) . ( 0 + 1)) /. x) + (( fD ((( fdif (f2,h)) . 0 ),h)) /. x)) by Def6

        .= (((( fdif (f1,h)) . ( 0 + 1)) /. x) + ((( fdif (f2,h)) . ( 0 + 1)) /. x)) by Def6;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A7, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:10

    ((( fdif ((f1 - f2),h)) . (n + 1)) /. x) = (((( fdif (f1,h)) . (n + 1)) /. x) - ((( fdif (f2,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( fdif ((f1 - f2),h)) . ($1 + 1)) /. x) = (((( fdif (f1,h)) . ($1 + 1)) /. x) - ((( fdif (f2,h)) . ($1 + 1)) /. x));

      

       A1: X[ 0 ]

      proof

        let x;

        x in the carrier of V;

        then x in ( dom f1) & x in ( dom f2) by FUNCT_2:def 1;

        then x in (( dom f1) /\ ( dom f2)) by XBOOLE_0:def 4;

        then

         A2: x in ( dom (f1 - f2)) by VFUNCT_1:def 2;

        (x + h) in the carrier of V;

        then (x + h) in ( dom f1) & (x + h) in ( dom f2) by FUNCT_2:def 1;

        then (x + h) in (( dom f1) /\ ( dom f2)) by XBOOLE_0:def 4;

        then

         A3: (x + h) in ( dom (f1 - f2)) by VFUNCT_1:def 2;

        ((( fdif ((f1 - f2),h)) . ( 0 + 1)) /. x) = (( fD ((( fdif ((f1 - f2),h)) . 0 ),h)) /. x) by Def6

        .= (( fD ((f1 - f2),h)) /. x) by Def6

        .= (((f1 - f2) /. (x + h)) - ((f1 - f2) /. x)) by Th3

        .= (((f1 /. (x + h)) - (f2 /. (x + h))) - ((f1 - f2) /. x)) by A3, VFUNCT_1:def 2

        .= (((f1 /. (x + h)) - (f2 /. (x + h))) - ((f1 /. x) - (f2 /. x))) by A2, VFUNCT_1:def 2

        .= ((((f1 /. (x + h)) - (f2 /. (x + h))) - (f1 /. x)) + (f2 /. x)) by RLVECT_1: 29

        .= (((f1 /. (x + h)) - ((f1 /. x) + (f2 /. (x + h)))) + (f2 /. x)) by RLVECT_1: 27

        .= ((((f1 /. (x + h)) - (f1 /. x)) - (f2 /. (x + h))) + (f2 /. x)) by RLVECT_1: 27

        .= (((( fD (f1,h)) /. x) - (f2 /. (x + h))) + (f2 /. x)) by Th3

        .= ((( fD (f1,h)) . x) - ((f2 /. (x + h)) - (f2 /. x))) by RLVECT_1: 29

        .= ((( fD (f1,h)) /. x) - (( fD (f2,h)) /. x)) by Th3

        .= ((( fD ((( fdif (f1,h)) . 0 ),h)) /. x) - (( fD (f2,h)) /. x)) by Def6

        .= ((( fD ((( fdif (f1,h)) . 0 ),h)) /. x) - (( fD ((( fdif (f2,h)) . 0 ),h)) /. x)) by Def6

        .= (((( fdif (f1,h)) . ( 0 + 1)) /. x) - (( fD ((( fdif (f2,h)) . 0 ),h)) /. x)) by Def6

        .= (((( fdif (f1,h)) . ( 0 + 1)) /. x) - ((( fdif (f2,h)) . ( 0 + 1)) /. x)) by Def6;

        hence thesis;

      end;

      

       A4: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A5: for x holds ((( fdif ((f1 - f2),h)) . (k + 1)) /. x) = (((( fdif (f1,h)) . (k + 1)) /. x) - ((( fdif (f2,h)) . (k + 1)) /. x));

        let x;

        

         A6: ((( fdif ((f1 - f2),h)) . (k + 1)) /. x) = (((( fdif (f1,h)) . (k + 1)) /. x) - ((( fdif (f2,h)) . (k + 1)) /. x)) & ((( fdif ((f1 - f2),h)) . (k + 1)) /. (x + h)) = (((( fdif (f1,h)) . (k + 1)) /. (x + h)) - ((( fdif (f2,h)) . (k + 1)) /. (x + h))) by A5;

        reconsider fd12k1 = (( fdif ((f1 - f2),h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fd2k = (( fdif (f2,h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fd1k = (( fdif (f1,h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fdiff12 = (( fdif ((f1 - f2),h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fdiff2 = (( fdif (f2,h)) . (k + 1)) as Function of V, W by Th2;

        reconsider fdiff1 = (( fdif (f1,h)) . (k + 1)) as Function of V, W by Th2;

        

         A12: (( fD ((( fdif (f1,h)) . (k + 1)),h)) /. x) = (( fD (fdiff1,h)) /. x)

        .= (((( fdif (f1,h)) . (k + 1)) /. (x + h)) - ((( fdif (f1,h)) . (k + 1)) /. x)) by Th3;

        

         A13: (( fD ((( fdif (f2,h)) . (k + 1)),h)) /. x) = (( fD (fdiff2,h)) /. x)

        .= (((( fdif (f2,h)) . (k + 1)) /. (x + h)) - ((( fdif (f2,h)) . (k + 1)) /. x)) by Th3;

        ((( fdif ((f1 - f2),h)) . ((k + 1) + 1)) /. x) = (( fD ((( fdif ((f1 - f2),h)) . (k + 1)),h)) /. x) by Def6

        .= ((fd12k1 /. (x + h)) - (fd12k1 /. x)) by Th3

        .= (((((( fdif (f1,h)) . (k + 1)) /. (x + h)) + ( - ((( fdif (f2,h)) . (k + 1)) /. (x + h)))) - ((( fdif (f1,h)) . (k + 1)) /. x)) + ((( fdif (f2,h)) . (k + 1)) /. x)) by RLVECT_1: 29, A6

        .= ((((( fdif (f1,h)) . (k + 1)) /. (x + h)) + (( - ((( fdif (f2,h)) . (k + 1)) /. (x + h))) + ( - ((( fdif (f1,h)) . (k + 1)) /. x)))) + ((( fdif (f2,h)) . (k + 1)) /. x)) by RLVECT_1:def 3

        .= (((((( fdif (f1,h)) . (k + 1)) /. (x + h)) + ( - ((( fdif (f1,h)) . (k + 1)) /. x))) - ((( fdif (f2,h)) . (k + 1)) /. (x + h))) + ((( fdif (f2,h)) . (k + 1)) /. x)) by RLVECT_1:def 3

        .= ((( fD ((( fdif (f1,h)) . (k + 1)),h)) /. x) - (((( fdif (f2,h)) . (k + 1)) /. (x + h)) - ((( fdif (f2,h)) . (k + 1)) /. x))) by A12, RLVECT_1: 29

        .= (((( fdif (f1,h)) . ((k + 1) + 1)) /. x) - (( fD ((( fdif (f2,h)) . (k + 1)),h)) /. x)) by Def6, A13

        .= (((( fdif (f1,h)) . ((k + 1) + 1)) /. x) - ((( fdif (f2,h)) . ((k + 1) + 1)) /. x)) by Def6;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A1, A4);

      hence thesis;

    end;

    theorem :: VSDIFF_1:11

    ((( fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x) = ((r1 * ((( fdif (f1,h)) . (n + 1)) /. x)) + (r2 * ((( fdif (f2,h)) . (n + 1)) /. x)))

    proof

      set g1 = (r1 (#) f1);

      set g2 = (r2 (#) f2);

      reconsider g1n1 = (( fdif (g1,h)) . (n + 1)) as Function of V, W by Th2;

      reconsider g2n1 = (( fdif (g2,h)) . (n + 1)) as Function of V, W by Th2;

      ((( fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x) = (((( fdif (g1,h)) . (n + 1)) /. x) + ((( fdif (g2,h)) . (n + 1)) /. x)) by Th8

      .= ((r1 * ((( fdif (f1,h)) . (n + 1)) /. x)) + ((( fdif (g2,h)) . (n + 1)) /. x)) by Th7

      .= ((r1 * ((( fdif (f1,h)) . (n + 1)) /. x)) + (r2 * ((( fdif (f2,h)) . (n + 1)) /. x))) by Th7;

      hence thesis;

    end;

    theorem :: VSDIFF_1:12

    ((( fdif (f,h)) . 1) /. x) = ((( Shift (f,h)) /. x) - (f /. x))

    proof

      set f1 = ( Shift (f,h));

      ((( fdif (f,h)) . 1) /. x) = ((( fdif (f,h)) . ( 0 + 1)) /. x)

      .= (( fD ((( fdif (f,h)) . 0 ),h)) /. x) by Def6

      .= (( fD (f,h)) /. x) by Def6

      .= ((f /. (x + h)) - (f /. x)) by Th3

      .= ((f1 /. x) - (f /. x)) by Def2;

      hence thesis;

    end;

    definition

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      :: VSDIFF_1:def9

      func backward_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means (it . 0 ) = f & for n be Nat holds (it . (n + 1)) = ( bD ((it . n),h));

      existence

      proof

        reconsider fZ = f as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

        defpred R[ set, set, set] means ex g be PartFunc of V, W st $2 = g & $3 = ( bD (g,h));

        

         A1: for n be Nat holds for x be Element of ( PFuncs (the carrier of V,the carrier of W)) holds ex y be Element of ( PFuncs (the carrier of V,the carrier of W)) st R[n, x, y]

        proof

          let n be Nat;

          let x be Element of ( PFuncs (the carrier of V,the carrier of W));

          reconsider x9 = x as PartFunc of V, W by PARTFUN1: 46;

          reconsider y = ( bD (x9,h)) as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

          ex w be PartFunc of V, W st x = w & y = ( bD (w,h));

          hence thesis;

        end;

        consider g be sequence of ( PFuncs (the carrier of V,the carrier of W)) such that

         A2: (g . 0 ) = fZ & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 2( A1);

        reconsider g as Functional_Sequence of the carrier of V, the carrier of W;

        take g;

        thus (g . 0 ) = f by A2;

        let i be Nat;

         R[i, (g . i), (g . (i + 1))] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Functional_Sequence of the carrier of V, the carrier of W;

        assume that

         A3: (seq1 . 0 ) = f and

         A4: for n be Nat holds (seq1 . (n + 1)) = ( bD ((seq1 . n),h)) and

         A5: (seq2 . 0 ) = f and

         A6: for n be Nat holds (seq2 . (n + 1)) = ( bD ((seq2 . n),h));

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

         A7: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume

           A8: P[k];

          

          thus (seq1 . (k + 1)) = ( bD ((seq1 . k),h)) by A4

          .= (seq2 . (k + 1)) by A6, A8;

        end;

        

         A9: P[ 0 ] by A3, A5;

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

        then for n be Element of NAT holds P[n];

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    definition

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      :: VSDIFF_1:def10

      func backward_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means

      : Def7: (it . 0 ) = f & for n be Nat holds (it . (n + 1)) = ( bD ((it . n),h));

      existence

      proof

        reconsider fZ = f as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

        defpred R[ set, set, set] means ex g be PartFunc of V, W st $2 = g & $3 = ( bD (g,h));

        

         A1: for n be Nat holds for x be Element of ( PFuncs (the carrier of V,the carrier of W)) holds ex y be Element of ( PFuncs (the carrier of V,the carrier of W)) st R[n, x, y]

        proof

          let n be Nat;

          let x be Element of ( PFuncs (the carrier of V,the carrier of W));

          reconsider x9 = x as PartFunc of V, W by PARTFUN1: 46;

          reconsider y = ( bD (x9,h)) as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

          ex w be PartFunc of V, W st x = w & y = ( bD (w,h));

          hence thesis;

        end;

        consider g be sequence of ( PFuncs (the carrier of V,the carrier of W)) such that

         A2: (g . 0 ) = fZ & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 2( A1);

        reconsider g as Functional_Sequence of the carrier of V, the carrier of W;

        take g;

        thus (g . 0 ) = f by A2;

        let i be Nat;

         R[i, (g . i), (g . (i + 1))] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Functional_Sequence of the carrier of V, the carrier of W;

        assume that

         A3: (seq1 . 0 ) = f and

         A4: for n be Nat holds (seq1 . (n + 1)) = ( bD ((seq1 . n),h)) and

         A5: (seq2 . 0 ) = f and

         A6: for n be Nat holds (seq2 . (n + 1)) = ( bD ((seq2 . n),h));

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

         A7: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume

           A8: P[k];

          

          thus (seq1 . (k + 1)) = ( bD ((seq1 . k),h)) by A4

          .= (seq2 . (k + 1)) by A6, A8;

        end;

        

         A9: P[ 0 ] by A3, A5;

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

        then for n be Element of NAT holds P[n];

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    notation

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be Function of V, W;

      synonym bdif (f,h) for backward_difference (f,h);

    end

    theorem :: VSDIFF_1:13

    

     Th12: for n be Nat holds (( bdif (f,h)) . n) is Function of V, W

    proof

      defpred X[ Nat] means (( bdif (f,h)) . $1) is Function of V, W;

      

       A1: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        assume (( bdif (f,h)) . k) is Function of V, W;

        then ( bD ((( bdif (f,h)) . k),h)) is Function of V, W;

        hence thesis by Def7;

      end;

      

       A2: X[ 0 ] by Def7;

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

      hence thesis;

    end;

    theorem :: VSDIFF_1:14

    f is constant implies for x holds ((( bdif (f,h)) . (n + 1)) /. x) = ( 0. W)

    proof

      assume

       A1: f is constant;

      

       A2: for x holds ((f /. x) - (f /. (x - h))) = ( 0. W)

      proof

        let x;

        (x - h) in the carrier of V;

        then

         A3: (x - h) in ( dom f) by FUNCT_2:def 1;

        x in the carrier of V;

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

        then (f /. x) = (f /. (x - h)) by A1, A3, FUNCT_1:def 10;

        hence thesis by RLVECT_1: 15;

      end;

      for x holds ((( bdif (f,h)) . (n + 1)) /. x) = ( 0. W)

      proof

        defpred X[ Nat] means for x holds ((( bdif (f,h)) . ($1 + 1)) /. x) = ( 0. W);

        

         A4: for k st X[k] holds X[(k + 1)]

        proof

          let k;

          assume

           A5: for x holds ((( bdif (f,h)) . (k + 1)) /. x) = ( 0. W);

          let x;

          

           A6: ((( bdif (f,h)) . (k + 1)) /. (x - h)) = ( 0. W) by A5;

          

           A7: (( bdif (f,h)) . (k + 1)) is Function of V, W by Th12;

          ((( bdif (f,h)) . (k + 2)) /. x) = ((( bdif (f,h)) . ((k + 1) + 1)) /. x)

          .= (( bD ((( bdif (f,h)) . (k + 1)),h)) /. x) by Def7

          .= (((( bdif (f,h)) . (k + 1)) /. x) - ((( bdif (f,h)) . (k + 1)) /. (x - h))) by A7, Th4

          .= (( 0. W) - ( 0. W)) by A5, A6

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

          hence thesis;

        end;

        

         A8: X[ 0 ]

        proof

          let x;

          

          thus ((( bdif (f,h)) . ( 0 + 1)) /. x) = (( bD ((( bdif (f,h)) . 0 ),h)) /. x) by Def7

          .= (( bD (f,h)) /. x) by Def7

          .= ((f /. x) - (f /. (x - h))) by Th4

          .= ( 0. W) by A2;

        end;

        for n holds X[n] from NAT_1:sch 2( A8, A4);

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: VSDIFF_1:15

    

     Th14: ((( bdif ((r (#) f),h)) . (n + 1)) /. x) = (r * ((( bdif (f,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( bdif ((r (#) f),h)) . ($1 + 1)) /. x) = (r * ((( bdif (f,h)) . ($1 + 1)) /. x));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( bdif ((r (#) f),h)) . (k + 1)) /. x) = (r * ((( bdif (f,h)) . (k + 1)) /. x));

        let x;

        

         A3: ((( bdif ((r (#) f),h)) . (k + 1)) /. x) = (r * ((( bdif (f,h)) . (k + 1)) /. x)) & ((( bdif ((r (#) f),h)) . (k + 1)) /. (x - h)) = (r * ((( bdif (f,h)) . (k + 1)) /. (x - h))) by A2;

        

         A4: (( bdif ((r (#) f),h)) . (k + 1)) is Function of V, W by Th12;

        

         A5: (( bdif (f,h)) . (k + 1)) is Function of V, W by Th12;

        ((( bdif ((r (#) f),h)) . ((k + 1) + 1)) /. x) = (( bD ((( bdif ((r (#) f),h)) . (k + 1)),h)) /. x) by Def7

        .= (((( bdif ((r (#) f),h)) . (k + 1)) /. x) - ((( bdif ((r (#) f),h)) . (k + 1)) /. (x - h))) by A4, Th4

        .= (r * (((( bdif (f,h)) . (k + 1)) /. x) - ((( bdif (f,h)) . (k + 1)) /. (x - h)))) by VECTSP_1: 23, A3

        .= (r * (( bD ((( bdif (f,h)) . (k + 1)),h)) /. x)) by A5, Th4

        .= (r * ((( bdif (f,h)) . ((k + 1) + 1)) /. x)) by Def7;

        hence thesis;

      end;

      

       A6: X[ 0 ]

      proof

        let x;

        x in the carrier of V;

        then

         A7: x in ( dom (r (#) f)) by FUNCT_2:def 1;

        (x - h) in the carrier of V;

        then

         A8: (x - h) in ( dom (r (#) f)) by FUNCT_2:def 1;

        ((( bdif ((r (#) f),h)) . ( 0 + 1)) /. x) = (( bD ((( bdif ((r (#) f),h)) . 0 ),h)) /. x) by Def7

        .= (( bD ((r (#) f),h)) /. x) by Def7

        .= (((r (#) f) /. x) - ((r (#) f) /. (x - h))) by Th4

        .= (((r (#) f) /. x) - (r * (f /. (x - h)))) by A8, Def4X

        .= ((r * (f /. x)) - (r * (f /. (x - h)))) by A7, Def4X

        .= (r * ((f /. x) - (f /. (x - h)))) by VECTSP_1: 23

        .= (r * (( bD (f,h)) /. x)) by Th4

        .= (r * (( bD ((( bdif (f,h)) . 0 ),h)) /. x)) by Def7

        .= (r * ((( bdif (f,h)) . ( 0 + 1)) /. x)) by Def7;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:16

    

     Th15: ((( bdif ((f1 + f2),h)) . (n + 1)) /. x) = (((( bdif (f1,h)) . (n + 1)) /. x) + ((( bdif (f2,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( bdif ((f1 + f2),h)) . ($1 + 1)) /. x) = (((( bdif (f1,h)) . ($1 + 1)) /. x) + ((( bdif (f2,h)) . ($1 + 1)) /. x));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( bdif ((f1 + f2),h)) . (k + 1)) /. x) = (((( bdif (f1,h)) . (k + 1)) /. x) + ((( bdif (f2,h)) . (k + 1)) /. x));

        let x;

        

         A3: ((( bdif ((f1 + f2),h)) . (k + 1)) /. x) = (((( bdif (f1,h)) . (k + 1)) /. x) + ((( bdif (f2,h)) . (k + 1)) /. x)) & ((( bdif ((f1 + f2),h)) . (k + 1)) /. (x - h)) = (((( bdif (f1,h)) . (k + 1)) /. (x - h)) + ((( bdif (f2,h)) . (k + 1)) /. (x - h))) by A2;

        

         A4: (( bdif ((f1 + f2),h)) . (k + 1)) is Function of V, W by Th12;

        

         A5: (( bdif (f2,h)) . (k + 1)) is Function of V, W by Th12;

        

         A6: (( bdif (f1,h)) . (k + 1)) is Function of V, W by Th12;

        ((( bdif ((f1 + f2),h)) . ((k + 1) + 1)) /. x) = (( bD ((( bdif ((f1 + f2),h)) . (k + 1)),h)) /. x) by Def7

        .= (((( bdif ((f1 + f2),h)) . (k + 1)) /. x) - ((( bdif ((f1 + f2),h)) . (k + 1)) /. (x - h))) by A4, Th4

        .= (((((( bdif (f2,h)) . (k + 1)) /. x) + ((( bdif (f1,h)) . (k + 1)) /. x)) - ((( bdif (f1,h)) . (k + 1)) /. (x - h))) - ((( bdif (f2,h)) . (k + 1)) /. (x - h))) by RLVECT_1: 27, A3

        .= ((((( bdif (f2,h)) . (k + 1)) /. x) + (((( bdif (f1,h)) . (k + 1)) /. x) - ((( bdif (f1,h)) . (k + 1)) /. (x - h)))) - ((( bdif (f2,h)) . (k + 1)) /. (x - h))) by RLVECT_1: 28

        .= ((((( bdif (f1,h)) . (k + 1)) /. x) - ((( bdif (f1,h)) . (k + 1)) /. (x - h))) + (((( bdif (f2,h)) . (k + 1)) /. x) - ((( bdif (f2,h)) . (k + 1)) /. (x - h)))) by RLVECT_1: 28

        .= ((( bD ((( bdif (f1,h)) . (k + 1)),h)) /. x) + (((( bdif (f2,h)) . (k + 1)) /. x) - ((( bdif (f2,h)) . (k + 1)) /. (x - h)))) by A6, Th4

        .= ((( bD ((( bdif (f1,h)) . (k + 1)),h)) /. x) + (( bD ((( bdif (f2,h)) . (k + 1)),h)) /. x)) by A5, Th4

        .= (((( bdif (f1,h)) . ((k + 1) + 1)) /. x) + (( bD ((( bdif (f2,h)) . (k + 1)),h)) /. x)) by Def7

        .= (((( bdif (f1,h)) . ((k + 1) + 1)) /. x) + ((( bdif (f2,h)) . ((k + 1) + 1)) /. x)) by Def7;

        hence thesis;

      end;

      

       A7: X[ 0 ]

      proof

        let x;

        reconsider xx = x, h as Element of V;

        

         B0: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 1

        .= (the carrier of V /\ ( dom f2)) by FUNCT_2:def 1

        .= (the carrier of V /\ the carrier of V) by FUNCT_2:def 1

        .= the carrier of V;

        ((( bdif ((f1 + f2),h)) . ( 0 + 1)) /. x) = (( bD ((( bdif ((f1 + f2),h)) . 0 ),h)) /. x) by Def7

        .= (( bD ((f1 + f2),h)) /. x) by Def7

        .= (((f1 + f2) /. x) - ((f1 + f2) /. (x - h))) by Th4

        .= (((f1 /. xx) + (f2 /. xx)) - ((f1 + f2) /. (xx - h))) by B0, VFUNCT_1:def 1

        .= (((f1 /. x) + (f2 /. x)) - ((f1 /. (x - h)) + (f2 /. (x - h)))) by B0, VFUNCT_1:def 1

        .= ((((f1 /. x) + (f2 /. x)) - (f1 /. (x - h))) - (f2 /. (x - h))) by RLVECT_1: 27

        .= (((f2 /. x) + ((f1 /. x) - (f1 /. (x - h)))) - (f2 /. (x - h))) by RLVECT_1: 28

        .= (((f1 /. x) - (f1 /. (x - h))) + ((f2 /. x) - (f2 /. (x - h)))) by RLVECT_1: 28

        .= ((( bD (f1,h)) /. x) + ((f2 /. x) - (f2 /. (x - h)))) by Th4

        .= ((( bD (f1,h)) /. x) + (( bD (f2,h)) /. x)) by Th4

        .= ((( bD ((( bdif (f1,h)) . 0 ),h)) /. x) + (( bD (f2,h)) /. x)) by Def7

        .= ((( bD ((( bdif (f1,h)) . 0 ),h)) /. x) + (( bD ((( bdif (f2,h)) . 0 ),h)) /. x)) by Def7

        .= (((( bdif (f1,h)) . ( 0 + 1)) /. x) + (( bD ((( bdif (f2,h)) . 0 ),h)) /. x)) by Def7

        .= (((( bdif (f1,h)) . ( 0 + 1)) /. x) + ((( bdif (f2,h)) . ( 0 + 1)) /. x)) by Def7;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A7, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:17

    ((( bdif ((f1 - f2),h)) . (n + 1)) /. x) = (((( bdif (f1,h)) . (n + 1)) /. x) - ((( bdif (f2,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( bdif ((f1 - f2),h)) . ($1 + 1)) /. x) = (((( bdif (f1,h)) . ($1 + 1)) /. x) - ((( bdif (f2,h)) . ($1 + 1)) /. x));

      

       A1: X[ 0 ]

      proof

        let x;

        x in the carrier of V;

        then x in ( dom f1) & x in ( dom f2) by FUNCT_2:def 1;

        then x in (( dom f1) /\ ( dom f2)) by XBOOLE_0:def 4;

        then

         A2: x in ( dom (f1 - f2)) by VFUNCT_1:def 2;

        (x - h) in the carrier of V;

        then (x - h) in ( dom f1) & (x - h) in ( dom f2) by FUNCT_2:def 1;

        then (x - h) in (( dom f1) /\ ( dom f2)) by XBOOLE_0:def 4;

        then

         A3: (x - h) in ( dom (f1 - f2)) by VFUNCT_1:def 2;

        ((( bdif ((f1 - f2),h)) . ( 0 + 1)) /. x) = (( bD ((( bdif ((f1 - f2),h)) . 0 ),h)) /. x) by Def7

        .= (( bD ((f1 - f2),h)) /. x) by Def7

        .= (((f1 - f2) /. x) - ((f1 - f2) /. (x - h))) by Th4

        .= (((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. (x - h))) by A2, VFUNCT_1:def 2

        .= (((f1 /. x) - (f2 /. x)) - ((f1 /. (x - h)) - (f2 /. (x - h)))) by A3, VFUNCT_1:def 2

        .= ((((f1 /. x) - (f2 /. x)) - (f1 /. (x - h))) + (f2 /. (x - h))) by RLVECT_1: 29

        .= (((f1 /. x) - ((f1 /. (x - h)) + (f2 /. x))) + (f2 /. (x - h))) by RLVECT_1: 27

        .= ((((f1 /. x) - (f1 /. (x - h))) - (f2 /. x)) + (f2 /. (x - h))) by RLVECT_1: 27

        .= (((f1 /. x) - (f1 /. (x - h))) - ((f2 /. x) - (f2 /. (x - h)))) by RLVECT_1: 29

        .= ((( bD (f1,h)) /. x) - ((f2 /. x) - (f2 /. (x - h)))) by Th4

        .= ((( bD (f1,h)) /. x) - (( bD (f2,h)) /. x)) by Th4

        .= ((( bD ((( bdif (f1,h)) . 0 ),h)) /. x) - (( bD (f2,h)) /. x)) by Def7

        .= ((( bD ((( bdif (f1,h)) . 0 ),h)) /. x) - (( bD ((( bdif (f2,h)) . 0 ),h)) /. x)) by Def7

        .= (((( bdif (f1,h)) . ( 0 + 1)) /. x) - (( bD ((( bdif (f2,h)) . 0 ),h)) /. x)) by Def7

        .= (((( bdif (f1,h)) . ( 0 + 1)) /. x) - ((( bdif (f2,h)) . ( 0 + 1)) /. x)) by Def7;

        hence thesis;

      end;

      

       A4: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A5: for x holds ((( bdif ((f1 - f2),h)) . (k + 1)) /. x) = (((( bdif (f1,h)) . (k + 1)) /. x) - ((( bdif (f2,h)) . (k + 1)) /. x));

        let x;

        

         A6: ((( bdif ((f1 - f2),h)) . (k + 1)) /. x) = (((( bdif (f1,h)) . (k + 1)) /. x) - ((( bdif (f2,h)) . (k + 1)) /. x)) & ((( bdif ((f1 - f2),h)) . (k + 1)) /. (x - h)) = (((( bdif (f1,h)) . (k + 1)) /. (x - h)) - ((( bdif (f2,h)) . (k + 1)) /. (x - h))) by A5;

        

         A7: (( bdif ((f1 - f2),h)) . (k + 1)) is Function of V, W by Th12;

        

         A8: (( bdif (f2,h)) . (k + 1)) is Function of V, W by Th12;

        

         A9: (( bdif (f1,h)) . (k + 1)) is Function of V, W by Th12;

        ((( bdif ((f1 - f2),h)) . ((k + 1) + 1)) /. x) = (( bD ((( bdif ((f1 - f2),h)) . (k + 1)),h)) /. x) by Def7

        .= (((( bdif ((f1 - f2),h)) . (k + 1)) /. x) - ((( bdif ((f1 - f2),h)) . (k + 1)) /. (x - h))) by A7, Th4

        .= (((((( bdif (f1,h)) . (k + 1)) /. x) - ((( bdif (f2,h)) . (k + 1)) /. x)) - ((( bdif (f1,h)) . (k + 1)) /. (x - h))) + ((( bdif (f2,h)) . (k + 1)) /. (x - h))) by RLVECT_1: 29, A6

        .= ((((( bdif (f1,h)) . (k + 1)) /. x) - (((( bdif (f1,h)) . (k + 1)) /. (x - h)) + ((( bdif (f2,h)) . (k + 1)) /. x))) + ((( bdif (f2,h)) . (k + 1)) /. (x - h))) by RLVECT_1: 27

        .= (((((( bdif (f1,h)) . (k + 1)) /. x) - ((( bdif (f1,h)) . (k + 1)) /. (x - h))) - ((( bdif (f2,h)) . (k + 1)) /. x)) + ((( bdif (f2,h)) . (k + 1)) /. (x - h))) by RLVECT_1: 27

        .= ((((( bdif (f1,h)) . (k + 1)) /. x) - ((( bdif (f1,h)) . (k + 1)) /. (x - h))) - (((( bdif (f2,h)) . (k + 1)) /. x) - ((( bdif (f2,h)) . (k + 1)) /. (x - h)))) by RLVECT_1: 29

        .= ((( bD ((( bdif (f1,h)) . (k + 1)),h)) /. x) - (((( bdif (f2,h)) . (k + 1)) /. x) - ((( bdif (f2,h)) . (k + 1)) /. (x - h)))) by A9, Th4

        .= ((( bD ((( bdif (f1,h)) . (k + 1)),h)) /. x) - (( bD ((( bdif (f2,h)) . (k + 1)),h)) /. x)) by A8, Th4

        .= (((( bdif (f1,h)) . ((k + 1) + 1)) /. x) - (( bD ((( bdif (f2,h)) . (k + 1)),h)) /. x)) by Def7

        .= (((( bdif (f1,h)) . ((k + 1) + 1)) /. x) - ((( bdif (f2,h)) . ((k + 1) + 1)) /. x)) by Def7;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A1, A4);

      hence thesis;

    end;

    theorem :: VSDIFF_1:18

    ((( bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x) = ((r1 * ((( bdif (f1,h)) . (n + 1)) /. x)) + (r2 * ((( bdif (f2,h)) . (n + 1)) /. x)))

    proof

      set g1 = (r1 (#) f1);

      set g2 = (r2 (#) f2);

      ((( bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x) = (((( bdif (g1,h)) . (n + 1)) /. x) + ((( bdif (g2,h)) . (n + 1)) /. x)) by Th15

      .= ((r1 * ((( bdif (f1,h)) . (n + 1)) /. x)) + ((( bdif (g2,h)) . (n + 1)) /. x)) by Th14

      .= ((r1 * ((( bdif (f1,h)) . (n + 1)) /. x)) + (r2 * ((( bdif (f2,h)) . (n + 1)) /. x))) by Th14;

      hence thesis;

    end;

    theorem :: VSDIFF_1:19

    ((( bdif (f,h)) . 1) /. x) = ((f /. x) - (( Shift (f,( - h))) /. x))

    proof

      set f2 = ( Shift (f,( - h)));

      ((( bdif (f,h)) . 1) /. x) = ((( bdif (f,h)) . ( 0 + 1)) /. x)

      .= (( bD ((( bdif (f,h)) . 0 ),h)) /. x) by Def7

      .= (( bD (f,h)) /. x) by Def7

      .= ((f /. x) - (f /. (x - h))) by Th4

      .= ((f /. x) - (f2 /. x)) by Def2;

      hence thesis;

    end;

    definition

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be PartFunc of V, W;

      :: VSDIFF_1:def11

      func central_difference (f,h) -> Functional_Sequence of the carrier of V, the carrier of W means

      : Def8: (it . 0 ) = f & for n be Nat holds (it . (n + 1)) = ( cD ((it . n),h));

      existence

      proof

        reconsider fZ = f as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

        defpred R[ set, set, set] means ex g be PartFunc of V, W st $2 = g & $3 = ( cD (g,h));

        

         A1: for n be Nat holds for x be Element of ( PFuncs (the carrier of V,the carrier of W)) holds ex y be Element of ( PFuncs (the carrier of V,the carrier of W)) st R[n, x, y]

        proof

          let n be Nat;

          let x be Element of ( PFuncs (the carrier of V,the carrier of W));

          reconsider x9 = x as PartFunc of V, W by PARTFUN1: 46;

          reconsider y = ( cD (x9,h)) as Element of ( PFuncs (the carrier of V,the carrier of W)) by PARTFUN1: 45;

          ex w be PartFunc of V, W st x = w & y = ( cD (w,h));

          hence thesis;

        end;

        consider g be sequence of ( PFuncs (the carrier of V,the carrier of W)) such that

         A2: (g . 0 ) = fZ & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 2( A1);

        reconsider g as Functional_Sequence of the carrier of V, the carrier of W;

        take g;

        thus (g . 0 ) = f by A2;

        let i be Nat;

         R[i, (g . i), (g . (i + 1))] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be Functional_Sequence of the carrier of V, the carrier of W;

        assume that

         A3: (seq1 . 0 ) = f and

         A4: for n be Nat holds (seq1 . (n + 1)) = ( cD ((seq1 . n),h)) and

         A5: (seq2 . 0 ) = f and

         A6: for n be Nat holds (seq2 . (n + 1)) = ( cD ((seq2 . n),h));

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

         A7: for k st P[k] holds P[(k + 1)]

        proof

          let k;

          assume

           A8: P[k];

          

          thus (seq1 . (k + 1)) = ( cD ((seq1 . k),h)) by A4

          .= (seq2 . (k + 1)) by A6, A8;

        end;

        

         A9: P[ 0 ] by A3, A5;

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

        then for n be Element of NAT holds P[n];

        hence seq1 = seq2 by FUNCT_2: 63;

      end;

    end

    notation

      let F,G be Field;

      let V be VectSp of F;

      let h be Element of V;

      let W be VectSp of G;

      let f be PartFunc of V, W;

      synonym cdif (f,h) for central_difference (f,h);

    end

    theorem :: VSDIFF_1:20

    

     Th19: for n be Nat holds (( cdif (f,h)) . n) is Function of V, W

    proof

      defpred X[ Nat] means (( cdif (f,h)) . $1) is Function of V, W;

      

       A1: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat;

        assume (( cdif (f,h)) . k) is Function of V, W;

        then ( cD ((( cdif (f,h)) . k),h)) is Function of V, W;

        hence thesis by Def8;

      end;

      

       A2: X[ 0 ] by Def8;

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

      hence thesis;

    end;

    theorem :: VSDIFF_1:21

    f is constant implies for x holds ((( cdif (f,h)) . (n + 1)) /. x) = ( 0. W)

    proof

      defpred X[ Nat] means for x holds ((( cdif (f,h)) . ($1 + 1)) /. x) = ( 0. W);

      assume

       A1: f is constant;

      

       A2: for x holds ((f /. (x + (((2 * ( 1. F)) " ) * h))) - (f /. (x - (((2 * ( 1. F)) " ) * h)))) = ( 0. W)

      proof

        let x;

        (x - (((2 * ( 1. F)) " ) * h)) in the carrier of V;

        then

         A3: (x - (((2 * ( 1. F)) " ) * h)) in ( dom f) by FUNCT_2:def 1;

        (x + (((2 * ( 1. F)) " ) * h)) in the carrier of V;

        then (x + (((2 * ( 1. F)) " ) * h)) in ( dom f) by FUNCT_2:def 1;

        then (f /. (x + (((2 * ( 1. F)) " ) * h))) = (f /. (x - (((2 * ( 1. F)) " ) * h))) by A1, A3, FUNCT_1:def 10;

        hence thesis by RLVECT_1: 15;

      end;

      

       A4: X[ 0 ]

      proof

        let x;

        

        thus ((( cdif (f,h)) . ( 0 + 1)) /. x) = (( cD ((( cdif (f,h)) . 0 ),h)) /. x) by Def8

        .= (( cD (f,h)) /. x) by Def8

        .= ((f /. (x + (((2 * ( 1. F)) " ) * h))) - (f /. (x - (((2 * ( 1. F)) " ) * h)))) by Th5

        .= ( 0. W) by A2;

      end;

      

       A5: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A6: for x holds ((( cdif (f,h)) . (k + 1)) /. x) = ( 0. W);

        let x;

        

         A8: (( cdif (f,h)) . (k + 1)) is Function of V, W by Th19;

        ((( cdif (f,h)) . (k + 2)) /. x) = ((( cdif (f,h)) . ((k + 1) + 1)) /. x)

        .= (( cD ((( cdif (f,h)) . (k + 1)),h)) /. x) by Def8

        .= (((( cdif (f,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by A8, Th5

        .= (((( cdif (f,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ( 0. W)) by A6

        .= ((( cdif (f,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) by RLVECT_1: 13

        .= ( 0. W) by A6;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A4, A5);

      hence thesis;

    end;

    theorem :: VSDIFF_1:22

    

     Th21: ((( cdif ((r (#) f),h)) . (n + 1)) /. x) = (r * ((( cdif (f,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( cdif ((r (#) f),h)) . ($1 + 1)) /. x) = (r * ((( cdif (f,h)) . ($1 + 1)) /. x));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( cdif ((r (#) f),h)) . (k + 1)) /. x) = (r * ((( cdif (f,h)) . (k + 1)) /. x));

        let x;

        

         A3: ((( cdif ((r (#) f),h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))) = (r * ((( cdif (f,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) & ((( cdif ((r (#) f),h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) = (r * ((( cdif (f,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h)))) by A2;

        

         A4: (( cdif ((r (#) f),h)) . (k + 1)) is Function of V, W by Th19;

        

         A5: (( cdif (f,h)) . (k + 1)) is Function of V, W by Th19;

        ((( cdif ((r (#) f),h)) . ((k + 1) + 1)) /. x) = (( cD ((( cdif ((r (#) f),h)) . (k + 1)),h)) /. x) by Def8

        .= (((( cdif ((r (#) f),h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif ((r (#) f),h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by A4, Th5

        .= (r * (((( cdif (f,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) by VECTSP_1: 23, A3

        .= (r * (( cD ((( cdif (f,h)) . (k + 1)),h)) /. x)) by A5, Th5

        .= (r * ((( cdif (f,h)) . ((k + 1) + 1)) /. x)) by Def8;

        hence thesis;

      end;

      

       A6: X[ 0 ]

      proof

        let x;

        (x + (((2 * ( 1. F)) " ) * h)) in the carrier of V;

        then

         A7: (x + (((2 * ( 1. F)) " ) * h)) in ( dom (r (#) f)) by FUNCT_2:def 1;

        (x - (((2 * ( 1. F)) " ) * h)) in the carrier of V;

        then

         A8: (x - (((2 * ( 1. F)) " ) * h)) in ( dom (r (#) f)) by FUNCT_2:def 1;

        ((( cdif ((r (#) f),h)) . ( 0 + 1)) /. x) = (( cD ((( cdif ((r (#) f),h)) . 0 ),h)) /. x) by Def8

        .= (( cD ((r (#) f),h)) /. x) by Def8

        .= (((r (#) f) /. (x + (((2 * ( 1. F)) " ) * h))) - ((r (#) f) /. (x - (((2 * ( 1. F)) " ) * h)))) by Th5

        .= ((r * (f /. (x + (((2 * ( 1. F)) " ) * h)))) - ((r (#) f) /. (x - (((2 * ( 1. F)) " ) * h)))) by A7, Def4X

        .= ((r * (f /. (x + (((2 * ( 1. F)) " ) * h)))) - (r * (f /. (x - (((2 * ( 1. F)) " ) * h))))) by A8, Def4X

        .= (r * ((f /. (x + (((2 * ( 1. F)) " ) * h))) - (f /. (x - (((2 * ( 1. F)) " ) * h))))) by VECTSP_1: 23

        .= (r * (( cD (f,h)) /. x)) by Th5

        .= (r * (( cD ((( cdif (f,h)) . 0 ),h)) /. x)) by Def8

        .= (r * ((( cdif (f,h)) . ( 0 + 1)) /. x)) by Def8;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:23

    

     Th22: ((( cdif ((f1 + f2),h)) . (n + 1)) /. x) = (((( cdif (f1,h)) . (n + 1)) /. x) + ((( cdif (f2,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( cdif ((f1 + f2),h)) . ($1 + 1)) /. x) = (((( cdif (f1,h)) . ($1 + 1)) /. x) + ((( cdif (f2,h)) . ($1 + 1)) /. x));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( cdif ((f1 + f2),h)) . (k + 1)) /. x) = (((( cdif (f1,h)) . (k + 1)) /. x) + ((( cdif (f2,h)) . (k + 1)) /. x));

        let x;

        

         A4: (( cdif ((f1 + f2),h)) . (k + 1)) is Function of V, W by Th19;

        

         A5: (( cdif (f2,h)) . (k + 1)) is Function of V, W by Th19;

        

         A6: (( cdif (f1,h)) . (k + 1)) is Function of V, W by Th19;

        ((( cdif ((f1 + f2),h)) . ((k + 1) + 1)) /. x) = (( cD ((( cdif ((f1 + f2),h)) . (k + 1)),h)) /. x) by Def8

        .= (((( cdif ((f1 + f2),h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif ((f1 + f2),h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by A4, Th5

        .= ((((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) + ((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h)))) - ((( cdif ((f1 + f2),h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by A2

        .= ((((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) + ((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h)))) - (((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))) + ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) by A2

        .= (((((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) + ((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h)))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) - ((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 27

        .= ((((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) + (((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) - ((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 28

        .= ((((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) + (((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) by RLVECT_1: 28

        .= ((( cD ((( cdif (f1,h)) . (k + 1)),h)) /. x) + (((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) by A6, Th5

        .= ((( cD ((( cdif (f1,h)) . (k + 1)),h)) /. x) + (( cD ((( cdif (f2,h)) . (k + 1)),h)) /. x)) by A5, Th5

        .= (((( cdif (f1,h)) . ((k + 1) + 1)) /. x) + (( cD ((( cdif (f2,h)) . (k + 1)),h)) /. x)) by Def8

        .= (((( cdif (f1,h)) . ((k + 1) + 1)) /. x) + ((( cdif (f2,h)) . ((k + 1) + 1)) /. x)) by Def8;

        hence thesis;

      end;

      

       B1: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 1

      .= (the carrier of V /\ ( dom f2)) by FUNCT_2:def 1

      .= (the carrier of V /\ the carrier of V) by FUNCT_2:def 1

      .= the carrier of V;

      

       A7: X[ 0 ]

      proof

        let x;

        reconsider xx = x, hp = (((2 * ( 1. F)) " ) * h) as Element of V;

        ((( cdif ((f1 + f2),h)) . ( 0 + 1)) /. x) = (( cD ((( cdif ((f1 + f2),h)) . 0 ),h)) /. x) by Def8

        .= (( cD ((f1 + f2),h)) /. x) by Def8

        .= (((f1 + f2) /. (x + (((2 * ( 1. F)) " ) * h))) - ((f1 + f2) /. (x - (((2 * ( 1. F)) " ) * h)))) by Th5

        .= (((f1 /. (xx + (((2 * ( 1. F)) " ) * h))) + (f2 /. (xx + hp))) - ((f1 + f2) /. (xx - hp))) by B1, VFUNCT_1:def 1

        .= (((f1 /. (x + (((2 * ( 1. F)) " ) * h))) + (f2 /. (x + hp))) - ((f1 /. (x - (((2 * ( 1. F)) " ) * h))) + (f2 /. (x - hp)))) by B1, VFUNCT_1:def 1

        .= ((((f1 /. (x + (((2 * ( 1. F)) " ) * h))) + (f2 /. (x + hp))) - (f1 /. (x - (((2 * ( 1. F)) " ) * h)))) - (f2 /. (x - hp))) by RLVECT_1: 27

        .= (((f2 /. (x + hp)) + ((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - (f1 /. (x - (((2 * ( 1. F)) " ) * h))))) - (f2 /. (x - hp))) by RLVECT_1: 28

        .= (((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - (f1 /. (x - (((2 * ( 1. F)) " ) * h)))) + ((f2 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x - (((2 * ( 1. F)) " ) * h))))) by RLVECT_1: 28

        .= ((( cD (f1,h)) /. x) + ((f2 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x - (((2 * ( 1. F)) " ) * h))))) by Th5

        .= ((( cD (f1,h)) /. x) + (( cD (f2,h)) /. x)) by Th5

        .= ((( cD ((( cdif (f1,h)) . 0 ),h)) /. x) + (( cD (f2,h)) /. x)) by Def8

        .= ((( cD ((( cdif (f1,h)) . 0 ),h)) /. x) + (( cD ((( cdif (f2,h)) . 0 ),h)) /. x)) by Def8

        .= (((( cdif (f1,h)) . ( 0 + 1)) /. x) + (( cD ((( cdif (f2,h)) . 0 ),h)) /. x)) by Def8

        .= (((( cdif (f1,h)) . ( 0 + 1)) /. x) + ((( cdif (f2,h)) . ( 0 + 1)) /. x)) by Def8;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A7, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:24

    ((( cdif ((f1 - f2),h)) . (n + 1)) /. x) = (((( cdif (f1,h)) . (n + 1)) /. x) - ((( cdif (f2,h)) . (n + 1)) /. x))

    proof

      defpred X[ Nat] means for x holds ((( cdif ((f1 - f2),h)) . ($1 + 1)) /. x) = (((( cdif (f1,h)) . ($1 + 1)) /. x) - ((( cdif (f2,h)) . ($1 + 1)) /. x));

      

       A1: X[ 0 ]

      proof

        let x;

        (x - (((2 * ( 1. F)) " ) * h)) in the carrier of V;

        then (x - (((2 * ( 1. F)) " ) * h)) in ( dom f1) & (x - (((2 * ( 1. F)) " ) * h)) in ( dom f2) by FUNCT_2:def 1;

        then (x - (((2 * ( 1. F)) " ) * h)) in (( dom f1) /\ ( dom f2)) by XBOOLE_0:def 4;

        then

         A2: (x - (((2 * ( 1. F)) " ) * h)) in ( dom (f1 - f2)) by VFUNCT_1:def 2;

        (x + (((2 * ( 1. F)) " ) * h)) in the carrier of V;

        then (x + (((2 * ( 1. F)) " ) * h)) in ( dom f1) & (x + (((2 * ( 1. F)) " ) * h)) in ( dom f2) by FUNCT_2:def 1;

        then (x + (((2 * ( 1. F)) " ) * h)) in (( dom f1) /\ ( dom f2)) by XBOOLE_0:def 4;

        then

         A3: (x + (((2 * ( 1. F)) " ) * h)) in ( dom (f1 - f2)) by VFUNCT_1:def 2;

        ((( cdif ((f1 - f2),h)) . ( 0 + 1)) /. x) = (( cD ((( cdif ((f1 - f2),h)) . 0 ),h)) /. x) by Def8

        .= (( cD ((f1 - f2),h)) /. x) by Def8

        .= (((f1 - f2) /. (x + (((2 * ( 1. F)) " ) * h))) - ((f1 - f2) /. (x - (((2 * ( 1. F)) " ) * h)))) by Th5

        .= (((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x + (((2 * ( 1. F)) " ) * h)))) - ((f1 - f2) /. (x - (((2 * ( 1. F)) " ) * h)))) by A3, VFUNCT_1:def 2

        .= (((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x + (((2 * ( 1. F)) " ) * h)))) - ((f1 /. (x - (((2 * ( 1. F)) " ) * h))) - (f2 /. (x - (((2 * ( 1. F)) " ) * h))))) by A2, VFUNCT_1:def 2

        .= ((((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x + (((2 * ( 1. F)) " ) * h)))) - (f1 /. (x - (((2 * ( 1. F)) " ) * h)))) + (f2 /. (x - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 29

        .= (((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - ((f1 /. (x - (((2 * ( 1. F)) " ) * h))) + (f2 /. (x + (((2 * ( 1. F)) " ) * h))))) + (f2 /. (x - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 27

        .= ((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - (((f1 /. (x - (((2 * ( 1. F)) " ) * h))) + (f2 /. (x + (((2 * ( 1. F)) " ) * h)))) - (f2 /. (x - (((2 * ( 1. F)) " ) * h))))) by RLVECT_1: 29

        .= ((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - ((f1 /. (x - (((2 * ( 1. F)) " ) * h))) + ((f2 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x - (((2 * ( 1. F)) " ) * h)))))) by RLVECT_1: 28

        .= (((f1 /. (x + (((2 * ( 1. F)) " ) * h))) - (f1 /. (x - (((2 * ( 1. F)) " ) * h)))) - ((f2 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x - (((2 * ( 1. F)) " ) * h))))) by RLVECT_1: 27

        .= ((( cD (f1,h)) /. x) - ((f2 /. (x + (((2 * ( 1. F)) " ) * h))) - (f2 /. (x - (((2 * ( 1. F)) " ) * h))))) by Th5

        .= ((( cD (f1,h)) /. x) - (( cD (f2,h)) /. x)) by Th5

        .= ((( cD ((( cdif (f1,h)) . 0 ),h)) /. x) - (( cD (f2,h)) /. x)) by Def8

        .= ((( cD ((( cdif (f1,h)) . 0 ),h)) /. x) - (( cD ((( cdif (f2,h)) . 0 ),h)) /. x)) by Def8

        .= (((( cdif (f1,h)) . ( 0 + 1)) /. x) - (( cD ((( cdif (f2,h)) . 0 ),h)) /. x)) by Def8

        .= (((( cdif (f1,h)) . ( 0 + 1)) /. x) - ((( cdif (f2,h)) . ( 0 + 1)) /. x)) by Def8;

        hence thesis;

      end;

      

       A4: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A5: for x holds ((( cdif ((f1 - f2),h)) . (k + 1)) /. x) = (((( cdif (f1,h)) . (k + 1)) /. x) - ((( cdif (f2,h)) . (k + 1)) /. x));

        let x;

        

         A6: ((( cdif ((f1 - f2),h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))) = (((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) & ((( cdif ((f1 - f2),h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) = (((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h)))) by A5;

        

         A7: (( cdif ((f1 - f2),h)) . (k + 1)) is Function of the carrier of V, the carrier of W by Th19;

        

         A8: (( cdif (f2,h)) . (k + 1)) is Function of the carrier of V, the carrier of W by Th19;

        

         A9: (( cdif (f1,h)) . (k + 1)) is Function of the carrier of V, the carrier of W by Th19;

        ((( cdif ((f1 - f2),h)) . ((k + 1) + 1)) /. x) = (( cD ((( cdif ((f1 - f2),h)) . (k + 1)),h)) /. x) by Def8

        .= (((( cdif ((f1 - f2),h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif ((f1 - f2),h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by A7, Th5

        .= (((((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h)))) - ((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) + ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 29, A6

        .= ((((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - (((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))) + ((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))))) + ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 27

        .= (((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))) + ((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h)))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) by RLVECT_1: 29

        .= (((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - (((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))) + (((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))))) by RLVECT_1: 28

        .= ((((( cdif (f1,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f1,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h)))) - (((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) by RLVECT_1: 27

        .= ((( cD ((( cdif (f1,h)) . (k + 1)),h)) /. x) - (((( cdif (f2,h)) . (k + 1)) /. (x + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f2,h)) . (k + 1)) /. (x - (((2 * ( 1. F)) " ) * h))))) by A9, Th5

        .= ((( cD ((( cdif (f1,h)) . (k + 1)),h)) /. x) - (( cD ((( cdif (f2,h)) . (k + 1)),h)) /. x)) by A8, Th5

        .= (((( cdif (f1,h)) . ((k + 1) + 1)) /. x) - (( cD ((( cdif (f2,h)) . (k + 1)),h)) /. x)) by Def8

        .= (((( cdif (f1,h)) . ((k + 1) + 1)) /. x) - ((( cdif (f2,h)) . ((k + 1) + 1)) /. x)) by Def8;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A1, A4);

      hence thesis;

    end;

    theorem :: VSDIFF_1:25

    ((( cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x) = ((r1 * ((( cdif (f1,h)) . (n + 1)) /. x)) + (r2 * ((( cdif (f2,h)) . (n + 1)) /. x)))

    proof

      set g1 = (r1 (#) f1);

      set g2 = (r2 (#) f2);

      ((( cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x) = (((( cdif (g1,h)) . (n + 1)) /. x) + ((( cdif (g2,h)) . (n + 1)) /. x)) by Th22

      .= ((r1 * ((( cdif (f1,h)) . (n + 1)) /. x)) + ((( cdif (g2,h)) . (n + 1)) /. x)) by Th21

      .= ((r1 * ((( cdif (f1,h)) . (n + 1)) /. x)) + (r2 * ((( cdif (f2,h)) . (n + 1)) /. x))) by Th21;

      hence thesis;

    end;

    theorem :: VSDIFF_1:26

    ((( cdif (f,h)) . 1) /. x) = ((( Shift (f,(((2 * ( 1. F)) " ) * h))) /. x) - (( Shift (f,( - (((2 * ( 1. F)) " ) * h)))) /. x))

    proof

      set f2 = ( Shift (f,( - (((2 * ( 1. F)) " ) * h))));

      set f1 = ( Shift (f,(((2 * ( 1. F)) " ) * h)));

      ((( cdif (f,h)) . 1) /. x) = ((( cdif (f,h)) . ( 0 + 1)) /. x)

      .= (( cD ((( cdif (f,h)) . 0 ),h)) /. x) by Def8

      .= (( cD (f,h)) /. x) by Def8

      .= ((f /. (x + (((2 * ( 1. F)) " ) * h))) - (f /. (x - (((2 * ( 1. F)) " ) * h)))) by Th5

      .= ((f1 /. x) - (f /. (x + ( - (((2 * ( 1. F)) " ) * h))))) by Def2

      .= ((f1 /. x) - (f2 /. x)) by Def2;

      hence thesis;

    end;

    theorem :: VSDIFF_1:27

    ((( fdif (f,h)) . n) /. x) = ((( bdif (f,h)) . n) /. (x + (n * h)))

    proof

      defpred X[ Nat] means for x holds ((( fdif (f,h)) . $1) /. x) = ((( bdif (f,h)) . $1) /. (x + ($1 * h)));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( fdif (f,h)) . k) /. x) = ((( bdif (f,h)) . k) /. (x + (k * h)));

        let x;

        

         A3: ((( fdif (f,h)) . k) /. (x + h)) = ((( bdif (f,h)) . k) /. ((x + h) + (k * h))) by A2;

        reconsider fdk = (( fdif (f,h)) . k) as Function of the carrier of V, the carrier of W by Th2;

        

         N2: ((k * h) + h) = ((k * h) + (1 * h)) by BINOM: 13

        .= ((k + 1) * h) by BINOM: 15;

        

         N3: (k * h) = ((k * h) + ( 0. V)) by RLVECT_1: 4

        .= ((k * h) + (h - h)) by RLVECT_1: 15

        .= (((k + 1) * h) - h) by N2, RLVECT_1: 28;

        

         A5: (( bdif (f,h)) . k) is Function of the carrier of V, the carrier of W by Th12;

        ((( fdif (f,h)) . (k + 1)) /. x) = (( fD (fdk,h)) /. x) by Def6

        .= ((fdk /. (x + h)) - (fdk /. x)) by Th3

        .= (((( bdif (f,h)) . k) /. ((x + h) + (k * h))) - ((( bdif (f,h)) . k) /. (x + (k * h)))) by A2, A3

        .= (((( bdif (f,h)) . k) /. (x + (h + (k * h)))) - ((( bdif (f,h)) . k) /. (x + (k * h)))) by RLVECT_1:def 3

        .= (((( bdif (f,h)) . k) /. (x + ((k + 1) * h))) - ((( bdif (f,h)) . k) /. ((x + ((k + 1) * h)) - h))) by RLVECT_1: 28, N3, N2

        .= (( bD ((( bdif (f,h)) . k),h)) /. (x + ((k + 1) * h))) by A5, Th4

        .= ((( bdif (f,h)) . (k + 1)) /. (x + ((k + 1) * h))) by Def7;

        hence thesis;

      end;

      

       A6: X[ 0 ]

      proof

        let x;

        ((( fdif (f,h)) . 0 ) /. x) = (f /. x) by Def6

        .= ((( bdif (f,h)) . 0 ) /. x) by Def7

        .= ((( bdif (f,h)) . 0 ) /. (x + ( 0. V))) by RLVECT_1: 4

        .= ((( bdif (f,h)) . 0 ) /. (x + ( 0 * h))) by BINOM: 12;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A6, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:28

    

     LAST0: ( 1. F) <> ( - ( 1. F)) implies ((( fdif (f,h)) . (2 * n)) /. x) = ((( cdif (f,h)) . (2 * n)) /. (x + (n * h)))

    proof

      assume

       AS: ( 1. F) <> ( - ( 1. F));

      defpred X[ Nat] means for x holds ((( fdif (f,h)) . (2 * $1)) /. x) = ((( cdif (f,h)) . (2 * $1)) /. (x + ($1 * h)));

      

       A1: for k st X[k] holds X[(k + 1)]

      proof

        let k;

        assume

         A2: for x holds ((( fdif (f,h)) . (2 * k)) /. x) = ((( cdif (f,h)) . (2 * k)) /. (x + (k * h)));

        let x;

        

         A31: (h + h) = ((1 * h) + h) by BINOM: 13

        .= ((1 * h) + (1 * h)) by BINOM: 13

        .= ((1 + 1) * h) by BINOM: 15;

        

         A32: (( 1. F) + ( 1. F)) = ((1 * ( 1. F)) + ( 1. F)) by BINOM: 13

        .= ((1 * ( 1. F)) + (1 * ( 1. F))) by BINOM: 13

        .= ((1 + 1) * ( 1. F)) by BINOM: 15

        .= (2 * ( 1. F));

        

         A33: (h + h) = ((( 1. F) * h) + h) by VECTSP_1:def 17

        .= ((( 1. F) * h) + (( 1. F) * h)) by VECTSP_1:def 17

        .= ((2 * ( 1. F)) * h) by A32, VECTSP_1:def 15;

        

         A30: (2 * ( 1. F)) <> ( 0. F)

        proof

          assume

           A301: (2 * ( 1. F)) = ( 0. F);

          (( 1. F) + ( 1. F)) = ((1 * ( 1. F)) + ( 1. F)) by BINOM: 13

          .= ((1 * ( 1. F)) + (1 * ( 1. F))) by BINOM: 13

          .= ((1 + 1) * ( 1. F)) by BINOM: 15

          .= ( 0. F) by A301;

          hence contradiction by AS, RLVECT_1:def 10;

        end;

        

         A34: ((((2 * ( 1. F)) " ) * h) + (((2 * ( 1. F)) " ) * h)) = (((2 * ( 1. F)) " ) * (h + h)) by VECTSP_1:def 14

        .= ((((2 * ( 1. F)) " ) * (2 * ( 1. F))) * h) by VECTSP_1:def 16, A33

        .= (( 1. F) * h) by A30, VECTSP_1:def 10

        .= h by VECTSP_1:def 17;

        

         A35: (((x + ((k + 1) * h)) - (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)) = (((x + ((k * h) + (1 * h))) - (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)) by BINOM: 15

        .= ((((x + (k * h)) + (1 * h)) - (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)) by RLVECT_1:def 3

        .= ((((x + (k * h)) + h) - (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)) by BINOM: 13

        .= (((x + (k * h)) + h) - ((((2 * ( 1. F)) " ) * h) + (((2 * ( 1. F)) " ) * h))) by RLVECT_1: 27

        .= ((x + (k * h)) + (h - h)) by RLVECT_1: 28, A34

        .= ((x + (k * h)) + ( 0. V)) by RLVECT_1: 15

        .= (x + (k * h)) by RLVECT_1: 4;

        

         A36: (((x + ((k + 1) * h)) + (((2 * ( 1. F)) " ) * h)) + (((2 * ( 1. F)) " ) * h)) = ((x + ((k + 1) * h)) + ((((2 * ( 1. F)) " ) * h) + (((2 * ( 1. F)) " ) * h))) by RLVECT_1:def 3

        .= (x + (((k + 1) * h) + h)) by RLVECT_1:def 3, A34

        .= (x + (((k + 1) * h) + (1 * h))) by BINOM: 13

        .= (x + (((k + 1) + 1) * h)) by BINOM: 15

        .= (x + ((k + 2) * h));

        

         A3: ((( fdif (f,h)) . (2 * k)) /. ((x + h) + h)) = ((( cdif (f,h)) . (2 * k)) /. (((x + h) + h) + (k * h))) by A2

        .= ((( cdif (f,h)) . (2 * k)) /. ((x + h) + (h + (k * h)))) by RLVECT_1:def 3

        .= ((( cdif (f,h)) . (2 * k)) /. (x + (h + (h + (k * h))))) by RLVECT_1:def 3

        .= ((( cdif (f,h)) . (2 * k)) /. (x + ((h + h) + (k * h)))) by RLVECT_1:def 3

        .= ((( cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h))) by BINOM: 15, A31;

        

         A4: ((( fdif (f,h)) . (2 * k)) /. (x + h)) = ((( cdif (f,h)) . (2 * k)) /. ((x + h) + (k * h))) by A2

        .= ((( cdif (f,h)) . (2 * k)) /. ((x + (1 * h)) + (k * h))) by BINOM: 13

        .= ((( cdif (f,h)) . (2 * k)) /. (x + ((1 * h) + (k * h)))) by RLVECT_1:def 3

        .= ((( cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h))) by BINOM: 15;

        set r3 = ((( cdif (f,h)) . (2 * k)) /. (x + (k * h)));

        set r2 = ((( cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h)));

        set r1 = ((( cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h)));

        

         A5: (( fdif (f,h)) . ((2 * k) + 1)) is Function of V, W by Th2;

        

         A6: (( cdif (f,h)) . (2 * k)) is Function of V, W by Th19;

        

         A7: (( cdif (f,h)) . ((2 * k) + 1)) is Function of V, W by Th19;

        

         A8: (( fdif (f,h)) . (2 * k)) is Function of V, W by Th2;

        

         A9: ((( cdif (f,h)) . ((2 * k) + 1)) /. ((x + ((k + 1) * h)) - (((2 * ( 1. F)) " ) * h))) = (( cD ((( cdif (f,h)) . (2 * k)),h)) /. ((x + ((k + 1) * h)) - (((2 * ( 1. F)) " ) * h))) by Def8

        .= (((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * ( 1. F)) " ) * h)) + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)))) by A6, Th5

        .= (((( cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) - ((((2 * ( 1. F)) " ) * h) - (((2 * ( 1. F)) " ) * h)))) - ((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 29

        .= (((( cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) - ( 0. V))) - ((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) - (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)))) by RLVECT_1: 15

        .= (((( cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h))) - ((( cdif (f,h)) . (2 * k)) /. (x + (k * h)))) by A35, RLVECT_1: 13;

        

         A10: ((( cdif (f,h)) . ((2 * k) + 1)) /. ((x + ((k + 1) * h)) + (((2 * ( 1. F)) " ) * h))) = (( cD ((( cdif (f,h)) . (2 * k)),h)) /. ((x + ((k + 1) * h)) + (((2 * ( 1. F)) " ) * h))) by Def8

        .= (((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * ( 1. F)) " ) * h)) + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)))) by A6, Th5

        .= (((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * ( 1. F)) " ) * h)) + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) + ((((2 * ( 1. F)) " ) * h) - (((2 * ( 1. F)) " ) * h))))) by RLVECT_1: 28

        .= (((( cdif (f,h)) . (2 * k)) /. (((x + ((k + 1) * h)) + (((2 * ( 1. F)) " ) * h)) + (((2 * ( 1. F)) " ) * h))) - ((( cdif (f,h)) . (2 * k)) /. ((x + ((k + 1) * h)) + ( 0. V)))) by RLVECT_1: 15

        .= (((( cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h))) - ((( cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h)))) by A36, RLVECT_1: 4;

        

         A11: ((( cdif (f,h)) . (2 * (k + 1))) /. (x + ((k + 1) * h))) = ((( cdif (f,h)) . (((2 * k) + 1) + 1)) /. (x + ((k + 1) * h)))

        .= (( cD ((( cdif (f,h)) . ((2 * k) + 1)),h)) /. (x + ((k + 1) * h))) by Def8

        .= ((r1 - r2) - (r2 - r3)) by A7, A10, A9, Th5;

        ((( fdif (f,h)) . (2 * (k + 1))) /. x) = ((( fdif (f,h)) . (((2 * k) + 1) + 1)) /. x)

        .= (( fD ((( fdif (f,h)) . ((2 * k) + 1)),h)) /. x) by Def6

        .= (((( fdif (f,h)) . ((2 * k) + 1)) /. (x + h)) - ((( fdif (f,h)) . ((2 * k) + 1)) /. x)) by A5, Th3

        .= ((( fD ((( fdif (f,h)) . (2 * k)),h)) /. (x + h)) - ((( fdif (f,h)) . ((2 * k) + 1)) /. x)) by Def6

        .= ((( fD ((( fdif (f,h)) . (2 * k)),h)) /. (x + h)) - (( fD ((( fdif (f,h)) . (2 * k)),h)) /. x)) by Def6

        .= ((((( fdif (f,h)) . (2 * k)) /. ((x + h) + h)) - ((( fdif (f,h)) . (2 * k)) /. (x + h))) - (( fD ((( fdif (f,h)) . (2 * k)),h)) /. x)) by A8, Th3

        .= ((((( fdif (f,h)) . (2 * k)) /. ((x + h) + h)) - ((( fdif (f,h)) . (2 * k)) /. (x + h))) - (((( fdif (f,h)) . (2 * k)) /. (x + h)) - ((( fdif (f,h)) . (2 * k)) /. x))) by A8, Th3

        .= ((((( cdif (f,h)) . (2 * k)) /. (x + ((k + 2) * h))) - ((( cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h)))) - (((( cdif (f,h)) . (2 * k)) /. (x + ((k + 1) * h))) - ((( cdif (f,h)) . (2 * k)) /. (x + (k * h))))) by A2, A3, A4;

        hence thesis by A11;

      end;

      

       A12: X[ 0 ]

      proof

        let x;

        ((( fdif (f,h)) . (2 * 0 )) /. x) = (f /. x) by Def6

        .= ((( cdif (f,h)) . (2 * 0 )) /. x) by Def8

        .= ((( cdif (f,h)) . (2 * 0 )) /. (x + ( 0. V))) by RLVECT_1: 4

        .= ((( cdif (f,h)) . (2 * 0 )) /. (x + ( 0 * h))) by BINOM: 12;

        hence thesis;

      end;

      for n holds X[n] from NAT_1:sch 2( A12, A1);

      hence thesis;

    end;

    theorem :: VSDIFF_1:29

    ( 1. F) <> ( - ( 1. F)) implies ((( fdif (f,h)) . ((2 * n) + 1)) /. x) = ((( cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * ( 1. F)) " ) * h)))

    proof

      assume

       AS: ( 1. F) <> ( - ( 1. F));

      

       A32: (( 1. F) + ( 1. F)) = ((1 * ( 1. F)) + ( 1. F)) by BINOM: 13

      .= ((1 * ( 1. F)) + (1 * ( 1. F))) by BINOM: 13

      .= ((1 + 1) * ( 1. F)) by BINOM: 15

      .= (2 * ( 1. F));

      

       A33: (h + h) = ((( 1. F) * h) + h) by VECTSP_1:def 17

      .= ((( 1. F) * h) + (( 1. F) * h)) by VECTSP_1:def 17

      .= ((2 * ( 1. F)) * h) by A32, VECTSP_1:def 15;

      

       A30: (2 * ( 1. F)) <> ( 0. F)

      proof

        assume

         A301: (2 * ( 1. F)) = ( 0. F);

        (( 1. F) + ( 1. F)) = ((1 * ( 1. F)) + ( 1. F)) by BINOM: 13

        .= ((1 * ( 1. F)) + (1 * ( 1. F))) by BINOM: 13

        .= ((1 + 1) * ( 1. F)) by BINOM: 15

        .= ( 0. F) by A301;

        hence contradiction by AS, RLVECT_1:def 10;

      end;

      

       A34: ((((2 * ( 1. F)) " ) * h) + (((2 * ( 1. F)) " ) * h)) = (((2 * ( 1. F)) " ) * (h + h)) by VECTSP_1:def 14

      .= ((((2 * ( 1. F)) " ) * (2 * ( 1. F))) * h) by VECTSP_1:def 16, A33

      .= (( 1. F) * h) by A30, VECTSP_1:def 10

      .= h by VECTSP_1:def 17;

      

       A52: (( cdif (f,h)) . (2 * n)) is Function of V, W by Th19;

      

       A35: (((x + (n * h)) + (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)) = ((x + (n * h)) + ((((2 * ( 1. F)) " ) * h) - (((2 * ( 1. F)) " ) * h))) by RLVECT_1: 28

      .= ((x + (n * h)) + ( 0. V)) by RLVECT_1: 15

      .= (x + (n * h)) by RLVECT_1: 4;

      

       A36: (((x + (n * h)) + (((2 * ( 1. F)) " ) * h)) + (((2 * ( 1. F)) " ) * h)) = ((x + (n * h)) + ((((2 * ( 1. F)) " ) * h) + (((2 * ( 1. F)) " ) * h))) by RLVECT_1:def 3

      .= (x + ((n * h) + h)) by RLVECT_1:def 3, A34

      .= (x + ((n * h) + (1 * h))) by BINOM: 13

      .= (x + ((n + 1) * h)) by BINOM: 15;

      

       A51: (( fdif (f,h)) . (2 * n)) is Function of V, W by Th2;

      

       A11: ((( cdif (f,h)) . ((2 * n) + 1)) /. ((x + (n * h)) + (((2 * ( 1. F)) " ) * h))) = (( cD ((( cdif (f,h)) . (2 * n)),h)) /. ((x + (n * h)) + (((2 * ( 1. F)) " ) * h))) by Def8

      .= (((( cdif (f,h)) . (2 * n)) /. (x + ((n + 1) * h))) - ((( cdif (f,h)) . (2 * n)) /. (((x + (n * h)) + (((2 * ( 1. F)) " ) * h)) - (((2 * ( 1. F)) " ) * h)))) by A36, Th5, A52

      .= (((( cdif (f,h)) . (2 * n)) /. (x + ((n * h) + (1 * h)))) - ((( cdif (f,h)) . (2 * n)) /. (x + (n * h)))) by BINOM: 15, A35

      .= (((( cdif (f,h)) . (2 * n)) /. (x + ((n * h) + h))) - ((( cdif (f,h)) . (2 * n)) /. (x + (n * h)))) by BINOM: 13

      .= (((( cdif (f,h)) . (2 * n)) /. ((x + h) + (n * h))) - ((( cdif (f,h)) . (2 * n)) /. (x + (n * h)))) by RLVECT_1:def 3

      .= (((( fdif (f,h)) . (2 * n)) /. (x + h)) - ((( cdif (f,h)) . (2 * n)) /. (x + (n * h)))) by LAST0, AS

      .= (((( fdif (f,h)) . (2 * n)) /. (x + h)) - ((( fdif (f,h)) . (2 * n)) /. x)) by LAST0, AS;

      ((( fdif (f,h)) . ((2 * n) + 1)) /. x) = (( fD ((( fdif (f,h)) . (2 * n)),h)) /. x) by Def6

      .= (((( fdif (f,h)) . (2 * n)) /. (x + h)) - ((( fdif (f,h)) . (2 * n)) /. x)) by Th3, A51;

      hence thesis by A11;

    end;