:: Difference of Function on Vector Space over $\mathbbF$
::  by Kenichi Arai , Ken Wakabayashi and Hiroyuki Okazaki
:: 
:: Received September 26, 2014
:: Copyright (c) 2014-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, STRUCT_0, NUMBERS, CARD_1, SUBSET_1, ARYTM_3, SUPINF_2,
      ARYTM_1, RELAT_1, MESFUNC1, FUNCT_1, VECTSP_1, FUNCT_7, DIFF_1, PARTFUN1,
      SEQFUNC, VALUED_1, MEMBER_1, TARSKI, NAT_1, FUNCT_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      NUMBERS, XCMPLX_0, NAT_1, SEQFUNC, STRUCT_0, ALGSTR_0, RLVECT_1,
      VECTSP_1, VFUNCT_1, BINOM;
 constructors NAT_1, RELSET_1, VECTSP_1, SEQFUNC, VFUNCT_1, BINOM, ALGSTR_1;
 registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, VECTSP_1, XBOOLE_0,
      PARTFUN1, ALGSTR_1, FUNCT_2, VFUNCT_1, NAT_1;
 requirements NUMERALS, SUBSET, ARITHM, BOOLE;
 definitions TARSKI;
 equalities ALGSTR_0;
 theorems FUNCT_2, RLVECT_1, TARSKI, VECTSP_1, PARTFUN1, FUNCT_1, XBOOLE_0,
      SUBSET_1, VFUNCT_1, BINOM;
 schemes NAT_1, PARTFUN2, RECDEF_1, SEQ_1, XBOOLE_0;

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;
  func r(#)f -> PartFunc of C,V means
  :Def4X:
  dom it = dom f &
  for c being 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 being Element of C holds c in dom F iff P[c] and
A2: for c being 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 being 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;
  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 being set such that
A1: for x being 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;
  func Shift (f,h) -> PartFunc of V,W means
  :Def1:
  dom it = (-h) ++ (dom f) &
  (for x being 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 being 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 being object st y in X holds y in dom F by A1; then
A2: X c= dom F by TARSKI:def 3;
    for y being 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 being 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 MEASURE624:
  for x being Element of V, A being 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 being 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;
  redefine 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 being 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 being 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;
  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;
  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;
  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;
  func forward_difference(f,h) ->
  Functional_Sequence of the carrier of V,the carrier of W means
  :Def6:
  it.0 = f & for n being 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 being PartFunc of V, W st $2 = g &
    $3 = fD(g,h);
A1: for n be Nat
    for x being Element of PFuncs(the carrier of V,the carrier of W)
    ex y being 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 being 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 being 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 being 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 Th01:
  for f being 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 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 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 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 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
  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 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 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
  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
  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
  (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;
  func backward_difference(f,h) ->
  Functional_Sequence of the carrier of V,the carrier of W means
  it.0 = f & for n being 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 being PartFunc of V,W
      st $2 = g & $3 = bD(g,h);
A1: for n being Nat for x being Element of PFuncs(the carrier of V,
    the carrier of W) ex y being 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 being 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 being 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 being 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;
  func backward_difference(f,h) ->
  Functional_Sequence of the carrier of V,the carrier of W means
  :Def7:
  it.0 = f & for n being 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 being PartFunc of V,W st $2 = g &
    $3 = bD(g,h);
A1: for n being Nat for x being Element of PFuncs((the carrier of V),
    (the carrier of W)) ex y being 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 being 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 being 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 being 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 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
  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 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 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
  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
  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
  (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;
  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 being PartFunc of V,W st $2 = g &
    $3 = cD(g,h);
A1: for n being Nat
    for x being Element of PFuncs((the carrier of V),(the carrier of W))
    ex y being 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 being 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 being 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 being 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 Th19:
  for n being 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
  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 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 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
  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
  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
  (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
  (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 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
  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;