:: The Binomial Theorem for Algebraic Structures
::  by Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000-2012 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 NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_3,
      ALGSTR_1, BINOP_1, LATTICES, GROUP_1, VECTSP_2, VECTSP_1, SUPINF_2,
      RELAT_1, FUNCT_1, ZFMISC_1, CARD_1, FUNCT_2, MCART_1, CARD_3, FINSEQ_1,
      STRUCT_0, XXREAL_0, PARTFUN1, NAT_1, NEWTON, ARYTM_1, ORDINAL4, FINSEQ_2,
      BINOM;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, STRUCT_0,
      ALGSTR_0, PARTFUN1, FUNCT_1, FUNCT_2, ORDINAL1, NAT_1, FINSEQ_1,
      RELSET_1, BINOP_1, ALGSTR_1, FINSEQ_2, VECTSP_1, VECTSP_2, GROUP_1,
      NEWTON, RLVECT_1, XTUPLE_0, MCART_1, POLYNOM1, XXREAL_0;
 constructors BINOP_1, REAL_1, NEWTON, ALGSTR_1, MONOID_0, POLYNOM1, RELSET_1,
      FVSUM_1, XTUPLE_0;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
      FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, INT_1, ALGSTR_0,
      CARD_1, FINSEQ_1, XTUPLE_0;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
 definitions BINOP_1, ALGSTR_0, XTUPLE_0;
 theorems TARSKI, FUNCT_2, VECTSP_1, RLVECT_1, ALGSTR_1, NAT_1, MCART_1,
      FINSEQ_1, GROUP_1, NEWTON, FINSEQ_2, FUNCT_1, ZFMISC_1, INT_1, RELAT_1,
      POLYNOM1, XBOOLE_0, XREAL_1, PARTFUN1, ORDINAL1, ALGSTR_0, CARD_1,
      FINSEQ_5, XTUPLE_0;
 schemes NAT_1, RECDEF_1, INT_1;

begin  :: Preliminaries

registration
  cluster Abelian right_add-cancelable -> left_add-cancelable for non empty
    addLoopStr;
  coherence
  proof
    let R be non empty addLoopStr;
    assume R is Abelian right_add-cancelable;
    then reconsider R as Abelian right_add-cancelable non empty addLoopStr;
    R is left_add-cancelable
    proof
      let a,b,c be Element of R;
      assume a + b = a + c;
      hence thesis by ALGSTR_0:def 4;
    end;
    hence thesis;
  end;
  cluster Abelian left_add-cancelable -> right_add-cancelable for non empty
    addLoopStr;
  coherence
  proof
    let R be non empty addLoopStr;
    assume R is Abelian left_add-cancelable;
    then reconsider R as Abelian left_add-cancelable non empty addLoopStr;
    R is right_add-cancelable
    proof
      let a,b,c be Element of R;
      assume b + a = c + a;
      hence thesis by ALGSTR_0:def 3;
    end;
    hence thesis;
  end;
end;

registration
  cluster right_zeroed right_complementable add-associative ->
    right_add-cancelable for non empty addLoopStr;
  coherence;
end;

registration
  cluster Abelian add-associative left_zeroed right_zeroed commutative
    associative add-cancelable distributive unital for
non empty doubleLoopStr;
  existence
  proof
    set R = the comRing;
    take R;
    thus thesis;
  end;
end;

theorem Th1:
  for R being right_zeroed left_add-cancelable left-distributive
  non empty doubleLoopStr, a being Element of R holds 0.R * a = 0.R
proof
  let R be right_zeroed left_add-cancelable left-distributive non empty
  doubleLoopStr, a be Element of R;
  0.R * a = (0.R + 0.R) * a by RLVECT_1:def 4
    .= 0.R * a + 0.R * a by VECTSP_1:def 3;
  then 0.R * a + 0.R * a = 0.R * a + 0.R by RLVECT_1:def 4;
  hence thesis by ALGSTR_0:def 3;
end;

theorem Th2:
  for R being left_zeroed right_add-cancelable right-distributive
  non empty doubleLoopStr, a being Element of R holds a * 0.R = 0.R
proof
  let R be left_zeroed right_add-cancelable right-distributive non empty
  doubleLoopStr, a be Element of R;
  a * 0.R = a * (0.R + 0.R) by ALGSTR_1:def 2
    .= a * 0.R + a * 0.R by VECTSP_1:def 2;
  then a * 0.R + a * 0.R = 0.R + a * 0.R by ALGSTR_1:def 2;
  hence thesis by ALGSTR_0:def 4;
end;

 Lm1:
now
  let C,D be non empty set, b be Element of D, F be Function of [:C,D:],D;
  thus ex g being Function of [:NAT,C:],D st for a being Element of C holds
  g.(0,a) = b & for n being Element of NAT holds g.(n+1,a) = F.(a,g.(n,a))
  proof
A1: for a being Element of C holds ex f being Function of NAT,D st f.0 =
  b & for n being Element of NAT holds f.(n+1) = F.(a,f.n)
  proof
    let a be Element of C;
    defpred P[Element of NAT,Element of D,Element of D] means $3 = F.(a,
    $2);
A2: for n being Element of NAT for x being Element of D ex y being
    Element of D st P[n,x,y];
    ex f being Function of NAT,D st f.0 = b & for n being Element of
    NAT holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2 (A2);
    hence thesis;
  end;
  ex g being Function of C,Funcs(NAT,D) st for a being Element of C
  holds ex f being Function of NAT,D st g.a = f & f.0 = b & for n being
  Element of NAT holds f.(n+1) = F.(a,f.n)
  proof
    set h = {[a,l] where a is Element of C, l is Element of Funcs(NAT,D) :
ex f being Function of NAT,D st f = l & f.0 = b & for n being Element of
    NAT holds f.(n+1) = F.(a,f.n) };
A3: now
      let x,y1,y2 be set;
      assume that
A4:   [x,y1] in h and
A5:   [x,y2] in h;
      consider a1 being Element of C, l1 being Element of Funcs(NAT,D)
      such that
A6:   [x,y1] = [a1,l1] and
A7:   ex f being Function of NAT,D st f = l1 & f.0 = b & for n
      being Element of NAT holds f.(n+1) = F.(a1,f.n) by A4;
      consider a2 being Element of C, l2 being Element of Funcs(NAT,D)
      such that
A8:   [x,y2] = [a2,l2] and
A9:   ex f being Function of NAT,D st f = l2 & f.0 = b & for n
      being Element of NAT holds f.(n+1) = F.(a2,f.n) by A5;
      consider f1 being Function of NAT,D such that
A10:  f1 = l1 and
A11:  f1.0 = b and
A12:  for n being Element of NAT holds f1.(n+1) = F.(a1,f1.n) by A7;
      consider f2 being Function of NAT,D such that
A13:  f2 = l2 and
A14:  f2.0 = b and
A15:  for n being Element of NAT holds f2.(n+1) = F.(a2,f2.n) by A9;
A16:  a1 = [a1,l1]`1
        .= [x,y1]`1 by A6
        .= x
        .= [x,y2]`1
        .= [a2,l2]`1 by A8
        .= a2;
A17:  now
        defpred P[Element of NAT] means f1.$1 = f2.$1;
        let x be set;
        assume x in NAT;
        then reconsider x9 = x as Element of NAT;
A18:    now
          let n be Element of NAT;
          assume
A19:      P[n];
          f1.(n+1) = F.(a2,f1.n) by A12,A16
            .= f2.(n+1) by A15,A19;
          hence P[n+1];
        end;
A20:    P[0] by A11,A14;
        for n being Element of NAT holds P[n] from NAT_1:sch 1(A20,A18);
        hence f1.x = f2.x9 .= f2.x;
      end;
A21:  NAT = dom f1 & NAT = dom f2 by FUNCT_2:def 1;
      thus y1 = [x,y1]`2
        .= [a1,l1]`2 by A6
        .= l1
        .= l2 by A10,A13,A21,A17,FUNCT_1:2
        .= [a2,l2]`2
        .= [x,y2]`2 by A8
        .= y2;
    end;
    now
      let x be set;
      assume x in h;
      then ex a being Element of C, l being Element of Funcs(NAT,D) st x =
      [a,l] & ex f being Function of NAT,D st f = l & f.0 = b & for n being
      Element of NAT holds f.(n+1) = F.(a,f.n);
      hence x in [:C,Funcs(NAT,D):] by ZFMISC_1:def 2;
    end;
    then reconsider h as Relation of C,Funcs(NAT,D) by TARSKI:def 3;
A22: for x being set holds x in C implies x in dom h
    proof
      let x be set;
      assume
A23:  x in C;
      then consider f being Function of NAT,D such that
A24:  f.0 = b & for n being Element of NAT holds f.(n+1) = F.(x,f
      .n) by A1;
      reconsider f9 = f as Element of Funcs(NAT,D) by FUNCT_2:8;
      [x,f9] in h by A23,A24;
      hence thesis by XTUPLE_0:def 12;
    end;
    for x being set holds x in dom h implies x in C;
    then dom h = C by A22,TARSKI:1;
    then reconsider h as Function of C,Funcs(NAT,D) by A3,FUNCT_1:def 1
,FUNCT_2:def 1;
    take h;
    for a being Element of C holds ex f being Function of NAT,D st h.
    a = f & f.0 = b & for n being Element of NAT holds f.(n+1) = F.(a,f.n)
    proof
      let a be Element of C;
      dom h = C by FUNCT_2:def 1;
      then [a,h.a] in h by FUNCT_1:1;
      then consider
      a9 being Element of C, l being Element of Funcs(NAT,D) such
      that
A25:  [a,h.a] = [a9,l] and
A26:  ex f9 being Function of NAT,D st f9 = l & f9.0 = b & for n
      being Element of NAT holds f9.(n+1) = F.(a9,f9.n);
A27:  h.a = [a,h.a]`2
        .= [a9,l]`2 by A25
        .= l;
      a = [a,h.a]`1
        .= [a9,l]`1 by A25
        .= a9;
      hence thesis by A26,A27;
    end;
    hence thesis;
  end;
  then consider g being Function of C,Funcs(NAT,D) such that
A28: for a being Element of C holds ex f being Function of NAT,D st
  g.a = f & f.0 = b & for n being Element of NAT holds f.(n+1) = F.(a,f.n);
  set h = { [[n,a],z] where n is Element of NAT, a is Element of C, z is
  Element of D : ex f being Function of NAT,D st f = g.a & z = f.n };
A29: now
    let x,y1,y2 be set;
    assume that
A30: [x,y1] in h and
A31: [x,y2] in h;
    consider n1 being Element of NAT, a1 being Element of C, z1 being
    Element of D such that
A32: [x,y1] = [[n1,a1],z1] and
A33: ex f1 being Function of NAT,D st f1 = g.a1 & z1 = f1.n1 by A30;
    consider n2 being Element of NAT, a2 being Element of C, z2 being
    Element of D such that
A34: [x,y2] = [[n2,a2],z2] and
A35: ex f2 being Function of NAT,D st f2 = g.a2 & z2 = f2.n2 by A31;
A36: [n1,a1] = [[n1,a1],z1]`1
      .= [x,y1]`1 by A32
      .= x
      .= [x,y2]`1
      .= [[n2,a2],z2]`1 by A34
      .= [n2,a2];
A37: a1 = [n1,a1]`2
      .= [n2,a2]`2 by A36
      .= a2;
A38: n1 = [n1,a1]`1
      .= [n2,a2]`1 by A36
      .= n2;
    thus y1 = [x,y1]`2
      .= [x,y2]`2 by A32,A33,A34,A35,A37,A38
      .= y2;
  end;
  now
    let x be set;
    assume x in h;
    then consider n1 being Element of NAT, a1 being Element of C, z1 being
    Element of D such that
A39: x = [[n1,a1],z1] and
    ex f1 being Function of NAT,D st f1 = g.a1 & z1 = f1.n1;
    [n1,a1] in [:NAT,C:] by ZFMISC_1:def 2;
    hence x in [:[:NAT,C:],D:] by A39,ZFMISC_1:def 2;
  end;
  then reconsider h as Relation of [:NAT,C:],D by TARSKI:def 3;
A40: for x being set holds x in [:NAT,C:] implies x in dom h
  proof
    let x be set;
    assume x in [:NAT,C:];
    then consider n,d being set such that
A41: n in NAT and
A42: d in C and
A43: x = [n,d] by ZFMISC_1:def 2;
    reconsider d as Element of C by A42;
    reconsider n as Element of NAT by A41;
    consider f9 being Function of NAT,D such that
A44: g.d = f9 and
    f9.0 = b and
    for n being Element of NAT holds f9.(n+1) = F.(d,f9.n) by A28;
    ex z being Element of D st ex f being Function of NAT,D st f = g.
    d & z = f.n
    proof
      take f9.n;
      take f9;
      thus thesis by A44;
    end;
    then consider z being Element of D such that
A45: ex f being Function of NAT,D st f = g.d & z = f.n;
    [x,z] in h by A43,A45;
    hence thesis by XTUPLE_0:def 12;
  end;
  for x being set holds x in dom h implies x in [:NAT,C:];
  then dom h = [:NAT,C:] by A40,TARSKI:1;
  then reconsider h as Function of [:NAT,C:],D by A29,FUNCT_1:def 1
,FUNCT_2:def 1;
  take h;
  for a being Element of C holds h.(0,a) = b & for n being Element of
  NAT holds h.(n+1,a) = F.(a,h.(n,a))
  proof
    let a be Element of C;
    consider f9 being Function of NAT,D such that
A46: g.a = f9 and
A47: f9.0 = b and
A48: for n being Element of NAT holds f9.(n+1) = F.(a,f9.n) by A28;
A49: now
      let k be Element of NAT;
      [k+1,a] in [:NAT,C:] by ZFMISC_1:def 2;
      then [k+1,a] in dom h by FUNCT_2:def 1;
      then consider u being set such that
A50:  [[k+1,a],u] in h by XTUPLE_0:def 12;
      [k,a] in [:NAT,C:] by ZFMISC_1:def 2;
      then [k,a] in dom h by FUNCT_2:def 1;
      then consider v being set such that
A51:  [[k,a],v] in h by XTUPLE_0:def 12;
      consider n being Element of NAT, d being Element of C, z being Element
      of D such that
A52:  [[k+1,a],u] = [[n,d],z] and
A53:  ex f1 being Function of NAT,D st f1 = g.d & z = f1.n by A50;
A54:  u = [[k+1,a],u]`2
        .= [[n,d],z]`2 by A52
        .= z;
      consider n1 being Element of NAT, d1 being Element of C, z1 being
      Element of D such that
A55:  [[k,a],v] = [[n1,d1],z1] and
A56:  ex f2 being Function of NAT,D st f2 = g.d1 & z1 = f2.n1 by A51;
A57:  v = [[k,a],v]`2
        .= [[n1,d1],z1]`2 by A55
        .= z1;
A58:  [k+1,a] = [[k+1,a],u]`1
        .= [[n,d],z]`1 by A52
        .= [n,d];
A59:  d = [n,d]`2
        .= [k+1,a]`2 by A58
        .= a;
A60:  [k,a] = [[k,a],v]`1
        .= [[n1,d1],z1]`1 by A55
        .= [n1,d1];
A61:  n1 = [n1,d1]`1
        .= [k,a]`1 by A60
        .= k;
A62:  d1 = [n1,d1]`2
        .= [k,a]`2 by A60
        .= a;
      n = [n,d]`1
        .= [k+1,a]`1 by A58
        .= k+1;
      hence h.(k+1,a) = f9.(k+1) by A46,A50,A53,A54,A59,FUNCT_1:1
        .= F.(a,z1) by A46,A48,A56,A61,A62
        .= F.(a,h.(k,a)) by A51,A57,FUNCT_1:1;
    end;
    [0,a] in [:NAT,C:] by ZFMISC_1:def 2;
    then [0,a] in dom h by FUNCT_2:def 1;
    then consider u being set such that
A63: [[0,a],u] in h by XTUPLE_0:def 12;
    consider n being Element of NAT, d being Element of C, z being Element
    of D such that
A64: [[0,a],u] = [[n,d],z] and
A65: ex f1 being Function of NAT,D st f1 = g.d & z = f1.n by A63;
A66: u = [[0,a],u]`2
      .= [[n,d],z]`2 by A64
      .= z;
A67: [0,a] = [[0,a],u]`1
      .= [[n,d],z]`1 by A64
      .= [n,d];
A68: d = [n,d]`2
      .= [0,a]`2 by A67
      .= a;
    n = [n,d]`1
      .= [0,a]`1 by A67
      .= 0;
    hence thesis by A46,A47,A63,A65,A66,A68,A49,FUNCT_1:1;
  end;
  hence thesis;
end;
end;

Lm2:
now let C,D be non empty set, b be Element of D, F be Function of [:D,C:],D;
  thus ex g being Function of [:C,NAT:],D st for a being
Element of C holds g.(a,0) = b & for n being Element of NAT holds g.(a,n+1)
  = F.(g.(a,n),a) proof
A1: for a being Element of C holds ex f being Function of NAT,D st f.0 =
  b & for n being Element of NAT holds f.(n+1) = F.(f.n,a)
  proof
    let a be Element of C;
    defpred P[Element of NAT,Element of D,Element of D] means $3 = F.($2
    ,a);
A2: for n being Element of NAT for x being Element of D ex y being
    Element of D st P[n,x,y];
    ex f being Function of NAT,D st f.0 = b & for n being Element of
    NAT holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2 (A2);
    hence thesis;
  end;
  ex g being Function of C,Funcs(NAT,D) st for a being Element of C
  holds ex f being Function of NAT,D st g.a = f & f.0 = b & for n being
  Element of NAT holds f.(n+1) = F.(f.n,a)
  proof
    set h = {[a,l] where a is Element of C, l is Element of Funcs(NAT,D) :
ex f being Function of NAT,D st f = l & f.0 = b & for n being Element of
    NAT holds f.(n+1) = F.(f.n,a) };
A3: now
      let x,y1,y2 be set;
      assume that
A4:   [x,y1] in h and
A5:   [x,y2] in h;
      consider a1 being Element of C, l1 being Element of Funcs(NAT,D)
      such that
A6:   [x,y1] = [a1,l1] and
A7:   ex f being Function of NAT,D st f = l1 & f.0 = b & for n
      being Element of NAT holds f.(n+1) = F.(f.n,a1) by A4;
      consider a2 being Element of C, l2 being Element of Funcs(NAT,D)
      such that
A8:   [x,y2] = [a2,l2] and
A9:   ex f being Function of NAT,D st f = l2 & f.0 = b & for n
      being Element of NAT holds f.(n+1) = F.(f.n,a2) by A5;
      consider f1 being Function of NAT,D such that
A10:  f1 = l1 and
A11:  f1.0 = b and
A12:  for n being Element of NAT holds f1.(n+1) = F.(f1.n,a1) by A7;
      consider f2 being Function of NAT,D such that
A13:  f2 = l2 and
A14:  f2.0 = b and
A15:  for n being Element of NAT holds f2.(n+1) = F.(f2.n,a2) by A9;
A16:  a1 = [a1,l1]`1
        .= [x,y1]`1 by A6
        .= x
        .= [x,y2]`1
        .= [a2,l2]`1 by A8
        .= a2;
A17:  now
        defpred P[Element of NAT] means f1.$1 = f2.$1;
        let x be set;
        assume x in NAT;
        then reconsider x9 = x as Element of NAT;
A18:    now
          let n be Element of NAT;
          assume
A19:      P[n];
          f1.(n+1) = F.(f1.n,a2) by A12,A16
            .= f2.(n+1) by A15,A19;
          hence P[n+1];
        end;
A20:    P[0] by A11,A14;
        for n being Element of NAT holds P[n] from NAT_1:sch 1(A20,A18 );
        hence f1.x = f2.x9 .= f2.x;
      end;
A21:  NAT = dom f1 & NAT = dom f2 by FUNCT_2:def 1;
      thus y1 = [x,y1]`2
        .= [a1,l1]`2 by A6
        .= l1
        .= l2 by A10,A13,A21,A17,FUNCT_1:2
        .= [a2,l2]`2
        .= [x,y2]`2 by A8
        .= y2;
    end;
    now
      let x be set;
      assume x in h;
      then ex a being Element of C, l being Element of Funcs(NAT,D) st x =
      [a,l] & ex f being Function of NAT,D st f = l & f.0 = b & for n being
      Element of NAT holds f.(n+1) = F.(f.n,a);
      hence x in [:C,Funcs(NAT,D):] by ZFMISC_1:def 2;
    end;
    then reconsider h as Relation of C,Funcs(NAT,D) by TARSKI:def 3;
A22: for x being set holds x in C implies x in dom h
    proof
      let x be set;
      assume
A23:  x in C;
      then consider f being Function of NAT,D such that
A24:  f.0 = b & for n being Element of NAT holds f.(n+1) = F.(f.n
      ,x) by A1;
      reconsider f9 = f as Element of Funcs(NAT,D) by FUNCT_2:8;
      [x,f9] in h by A23,A24;
      hence thesis by XTUPLE_0:def 12;
    end;
    for x being set holds x in dom h implies x in C;
    then dom h = C by A22,TARSKI:1;
    then reconsider h as Function of C,Funcs(NAT,D) by A3,FUNCT_1:def 1
,FUNCT_2:def 1;
    take h;
    for a being Element of C holds ex f being Function of NAT,D st h.
    a = f & f.0 = b & for n being Element of NAT holds f.(n+1) = F.(f.n,a)
    proof
      let a be Element of C;
      dom h = C by FUNCT_2:def 1;
      then [a,h.a] in h by FUNCT_1:1;
      then consider
      a9 being Element of C, l being Element of Funcs(NAT,D) such
      that
A25:  [a,h.a] = [a9,l] and
A26:  ex f9 being Function of NAT,D st f9 = l & f9.0 = b & for n
      being Element of NAT holds f9.(n+1) = F.(f9.n,a9);
A27:  h.a = [a,h.a]`2
        .= [a9,l]`2 by A25
        .= l;
      a = [a,h.a]`1
        .= [a9,l]`1 by A25
        .= a9;
      hence thesis by A26,A27;
    end;
    hence thesis;
  end;
  then consider g being Function of C,Funcs(NAT,D) such that
A28: for a being Element of C holds ex f being Function of NAT,D st
  g.a = f & f.0 = b & for n being Element of NAT holds f.(n+1) = F.(f.n,a);
  set h = { [[a,n],z] where n is Element of NAT, a is Element of C, z is
  Element of D : ex f being Function of NAT,D st f = g.a & z = f.n };
A29: now
    let x,y1,y2 be set;
    assume that
A30: [x,y1] in h and
A31: [x,y2] in h;
    consider n1 being Element of NAT, a1 being Element of C, z1 being
    Element of D such that
A32: [x,y1] = [[a1,n1],z1] and
A33: ex f1 being Function of NAT,D st f1 = g.a1 & z1 = f1.n1 by A30;
    consider n2 being Element of NAT, a2 being Element of C, z2 being
    Element of D such that
A34: [x,y2] = [[a2,n2],z2] and
A35: ex f2 being Function of NAT,D st f2 = g.a2 & z2 = f2.n2 by A31;
A36: [a1,n1] = [[a1,n1],z1]`1
      .= [x,y1]`1 by A32
      .= x
      .= [x,y2]`1
      .= [[a2,n2],z2]`1 by A34
      .= [a2,n2];
A37: n1 = [a1,n1]`2
      .= [a2,n2]`2 by A36
      .= n2;
A38: a1 = [a1,n1]`1
      .= [a2,n2]`1 by A36
      .= a2;
    thus y1 = [x,y1]`2
      .= [x,y2]`2 by A32,A33,A34,A35,A37,A38
      .= y2;
  end;
  now
    let x be set;
    assume x in h;
    then consider n1 being Element of NAT, a1 being Element of C, z1 being
    Element of D such that
A39: x = [[a1,n1],z1] and
    ex f1 being Function of NAT,D st f1 = g.a1 & z1 = f1.n1;
    [a1,n1] in [:C,NAT:] by ZFMISC_1:def 2;
    hence x in [:[:C,NAT:],D:] by A39,ZFMISC_1:def 2;
  end;
  then reconsider h as Relation of [:C,NAT:],D by TARSKI:def 3;
A40: for x being set holds x in [:C,NAT:] implies x in dom h
  proof
    let x be set;
    assume x in [:C,NAT:];
    then consider d,n being set such that
A41: d in C and
A42: n in NAT and
A43: x = [d,n] by ZFMISC_1:def 2;
    reconsider d as Element of C by A41;
    reconsider n as Element of NAT by A42;
    consider f9 being Function of NAT,D such that
A44: g.d = f9 and
    f9.0 = b and
    for n being Element of NAT holds f9.(n+1) = F.(f9.n,d) by A28;
    ex z being Element of D st ex f being Function of NAT,D st f = g.
    d & z = f.n
    proof
      take f9.n;
      take f9;
      thus thesis by A44;
    end;
    then consider z being Element of D such that
A45: ex f being Function of NAT,D st f = g.d & z = f.n;
    [x,z] in h by A43,A45;
    hence thesis by XTUPLE_0:def 12;
  end;
  for x being set holds x in dom h implies x in [:C,NAT:];
  then dom h = [:C,NAT:] by A40,TARSKI:1;
  then reconsider h as Function of [:C,NAT:],D by A29,FUNCT_1:def 1
,FUNCT_2:def 1;
  take h;
  for a being Element of C holds h.(a,0) = b & for n being Element of
  NAT holds h.(a,n+1) = F.(h.(a,n),a)
  proof
    let a be Element of C;
    consider f9 being Function of NAT,D such that
A46: g.a = f9 and
A47: f9.0 = b and
A48: for n being Element of NAT holds f9.(n+1) = F.(f9.n,a) by A28;
A49: now
      let k be Element of NAT;
      [a,k+1] in [:C,NAT:] by ZFMISC_1:def 2;
      then [a,k+1] in dom h by FUNCT_2:def 1;
      then consider u being set such that
A50:  [[a,k+1],u] in h by XTUPLE_0:def 12;
      [a,k] in [:C,NAT:] by ZFMISC_1:def 2;
      then [a,k] in dom h by FUNCT_2:def 1;
      then consider v being set such that
A51:  [[a,k],v] in h by XTUPLE_0:def 12;
      consider n1 being Element of NAT, d1 being Element of C, z1 being
      Element of D such that
A52:  [[a,k],v] = [[d1,n1],z1] and
A53:  ex f2 being Function of NAT,D st f2 = g.d1 & z1 = f2.n1 by A51;
A54:  v = [[a,k],v]`2
        .= [[d1,n1],z1]`2 by A52
        .= z1;
A55:  [a,k] = [[a,k],v]`1
        .= [[d1,n1],z1]`1 by A52
        .= [d1,n1];
A56:  n1 = [d1,n1]`2
        .= [a,k]`2 by A55
        .= k;
      consider f2 being Function of NAT,D such that
A57:  f2 = g.d1 and
A58:  z1 = f2.n1 by A53;
      consider n being Element of NAT, d being Element of C, z being Element
      of D such that
A59:  [[a,k+1],u] = [[d,n],z] and
A60:  ex f1 being Function of NAT,D st f1 = g.d & z = f1.n by A50;
A61:  [a,k+1] = [[a,k+1],u]`1
        .= [[d,n],z]`1 by A59
        .= [d,n];
A62:  n = [d,n]`2
        .= [a,k+1]`2 by A61
        .= k+1;
A63:  d1 = [d1,n1]`1
        .= [a,k]`1 by A55
        .= a;
A64:  d = [d,n]`1
        .= [a,k+1]`1 by A61
        .= a;
      u = [[a,k+1],u]`2
        .= [[d,n],z]`2 by A59
        .= z;
      hence h.(a,k+1) = f9.n by A46,A50,A60,A64,FUNCT_1:1
        .= F.(f2.n1,a) by A46,A48,A62,A57,A56,A63
        .= F.(h.(a,k),a) by A51,A58,A54,FUNCT_1:1;
    end;
    [a,0] in [:C,NAT:] by ZFMISC_1:def 2;
    then [a,0] in dom h by FUNCT_2:def 1;
    then consider u being set such that
A65: [[a,0],u] in h by XTUPLE_0:def 12;
    consider n being Element of NAT, d being Element of C, z being Element
    of D such that
A66: [[a,0],u] = [[d,n],z] and
A67: ex f1 being Function of NAT,D st f1 = g.d & z = f1.n by A65;
A68: u = [[a,0],u]`2
      .= [[d,n],z]`2 by A66
      .= z;
A69: [a,0] = [[a,0],u]`1
      .= [[d,n],z]`1 by A66
      .= [d,n];
A70: d = [d,n]`1
      .= [a,0]`1 by A69
      .= a;
    n = [d,n]`2
      .= [a,0]`2 by A69
      .= 0;
    hence thesis by A46,A47,A65,A67,A68,A70,A49,FUNCT_1:1;
  end;
  hence thesis;
end;
end;

begin  ::  On Finite Sequences

theorem Th3:
  for L being left_zeroed non empty addLoopStr, a being Element
  of L holds Sum <* a *> = a
proof
  let V be left_zeroed non empty addLoopStr, v be Element of V;
  reconsider a = v as Element of V;
  set S = <* v *>;
  consider f being Function of NAT, the carrier of V such that
A1: Sum(S) = f.(len S) and
A2: f.0 = 0.V & for j being Element of NAT for v being Element of V st j
  < len S & v = S.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
A3: len <* a *> = 1 by FINSEQ_1:39;
  0 < 1;
  then consider j being Element of NAT such that
A4: j < len S;
A5: S.(j + 1) = S.(0 + 1) by A3,A4,NAT_1:14
    .= v by FINSEQ_1:40;
  j = 0 by A3,A4,NAT_1:14;
  then f.1 = 0.V + v by A2,A5
    .= a by ALGSTR_1:def 2;
  hence thesis by A1,FINSEQ_1:39;
end;

theorem
  for R being left_zeroed right_add-cancelable right-distributive non
empty doubleLoopStr, a being Element of R, p being FinSequence of the carrier
  of R holds Sum(a * p) = a * Sum p
proof
  let R be left_zeroed right_add-cancelable right-distributive non empty
  doubleLoopStr, a be Element of R, p be FinSequence of the carrier of R;
  consider f being Function of NAT,the carrier of R such that
A1: Sum p = f.(len p) and
A2: f.0 = 0.R and
A3: for j being Element of NAT, v being Element of R st j < len p & v =
  p.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
  consider fa being Function of NAT,the carrier of R such that
A4: Sum(a * p) = fa.(len(a * p)) and
A5: fa.0 = 0.R and
A6: for j being Element of NAT, v being Element of R st j < len(a * p) &
  v = (a * p).(j + 1) holds fa.(j + 1) = fa.j + v by RLVECT_1:def 12;
  defpred P[Element of NAT] means a * f.$1 = fa.$1;
A7: Seg(len(a * p)) = dom(a * p) by FINSEQ_1:def 3
    .= dom p by POLYNOM1:def 1
    .= Seg(len p) by FINSEQ_1:def 3;
A8: now
    let j be Element of NAT;
    assume that
    0 <= j and
A9: j < len p;
    thus P[j] implies P[j+1]
    proof
A10:  0 + 1 <= j + 1 by XREAL_1:6;
A11:  j < len(a * p) by A7,A9,FINSEQ_1:6;
      then j + 1 <= len(a * p) by NAT_1:13;
      then j + 1 in Seg len(a * p) by A10,FINSEQ_1:1;
      then j + 1 in dom(a * p) by FINSEQ_1:def 3;
      then
A12:  (a * p)/.(j + 1) = (a * p).(j + 1) by PARTFUN1:def 6;
      j + 1 <= len p by A9,NAT_1:13;
      then j + 1 in Seg len p by A10,FINSEQ_1:1;
      then
A13:  j + 1 in dom p by FINSEQ_1:def 3;
      then
A14:  p/.(j + 1) = p.(j + 1) by PARTFUN1:def 6;
      assume P[j];
      hence fa.(j+1) = a * f.j + (a * p)/.(j + 1) by A6,A11,A12
        .= a * f.j + a * p/.(j + 1) by A13,POLYNOM1:def 1
        .= a * (f.j + p/.(j + 1)) by VECTSP_1:def 2
        .= a * f.(j+1) by A3,A9,A14;
    end;
  end;
A15: P[0] by A2,A5,Th2;
A16: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from
  INT_1:sch 7(A15,A8);
  thus Sum(a * p) = fa.(len p) by A4,A7,FINSEQ_1:6
    .= a * Sum p by A1,A16;
end;

theorem Th5:
  for R being right_zeroed left_add-cancelable left-distributive
  non empty doubleLoopStr, a being Element of R, p being FinSequence of the
  carrier of R holds Sum(p * a) = Sum p * a
proof
  let R be right_zeroed left_add-cancelable left-distributive non empty
  doubleLoopStr, a be Element of R, p be FinSequence of the carrier of R;
  consider f being Function of NAT,the carrier of R such that
A1: Sum p = f.(len p) and
A2: f.0 = 0.R and
A3: for j being Element of NAT, v being Element of R st j < len p & v =
  p.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
  consider fa being Function of NAT,the carrier of R such that
A4: Sum(p * a) = fa.(len(p * a)) and
A5: fa.0 = 0.R and
A6: for j being Element of NAT, v being Element of R st j < len(p * a) &
  v = (p * a).(j + 1) holds fa.(j + 1) = fa.j + v by RLVECT_1:def 12;
  defpred P[Element of NAT] means f.$1 * a = fa.$1;
A7: Seg(len(p * a)) = dom(p * a) by FINSEQ_1:def 3
    .= dom p by POLYNOM1:def 2
    .= Seg(len p) by FINSEQ_1:def 3;
A8: now
    let j be Element of NAT;
    assume that
    0 <= j and
A9: j < len p;
    thus P[j] implies P[j+1]
    proof
A10:  j < len(p * a) by A7,A9,FINSEQ_1:6;
      then
A11:  j + 1 <= len(p * a) by NAT_1:13;
A12:  0 + 1 <= j + 1 by XREAL_1:6;
      then j + 1 in Seg len(p * a) by A11,FINSEQ_1:1;
      then j + 1 in dom(p * a) by FINSEQ_1:def 3;
      then
A13:  (p * a)/.(j + 1) = (p * a).(j + 1) by PARTFUN1:def 6;
      j + 1 in Seg len p by A7,A11,A12,FINSEQ_1:1;
      then
A14:  j + 1 in dom p by FINSEQ_1:def 3;
      then
A15:  p/.(j + 1) = p.(j + 1) by PARTFUN1:def 6;
      assume f.j * a = fa.j;
      hence fa.(j+1) = f.j * a + (p * a)/.(j + 1) by A6,A10,A13
        .= f.j * a + p/.(j + 1) * a by A14,POLYNOM1:def 2
        .= (f.j + p/.(j + 1)) * a by VECTSP_1:def 3
        .= f.(j+1) * a by A3,A9,A15;
    end;
  end;
A16: P[0] by A2,A5,Th1;
A17: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from
  INT_1:sch 7(A16,A8);
  thus Sum(p * a) = fa.(len p) by A4,A7,FINSEQ_1:6
    .= Sum p * a by A1,A17;
end;

theorem
  for R being commutative non empty multMagma, a being Element of R,
  p being FinSequence of the carrier of R holds p * a = a * p
proof
  let R be commutative non empty multMagma, a be Element of R, p be
  FinSequence of the carrier of R;
  set pa = p*a, ap = a*p;
A1: dom pa = dom p by POLYNOM1:def 2;
A2: dom ap = dom p by POLYNOM1:def 1;
  now
    let i be Nat such that
A3: i in dom pa;
    thus pa/.i = p/.i * a by A1,A3,POLYNOM1:def 2
    .= ap/.i by A1,A3,POLYNOM1:def 1;
  end;
  hence thesis by A1,A2,FINSEQ_5:12;
end;

definition

  let R be non empty addLoopStr, p,q be FinSequence of the carrier of R;
  func p + q -> FinSequence of the carrier of R means
  :Def1:
  dom it = dom p &
  for i being Nat st 1 <= i & i <= len it holds it/.i = p/.i + q/.i;
  existence
  proof
    defpred P[Element of NAT,Element of R] means $2 = (p/.($1)) + (q/.($1));
A1: for k being Element of NAT st k in Seg(len p) ex x being Element of R
    st P[k,x];
    consider f being FinSequence of the carrier of R such that
A2: dom f = Seg(len p) & for k being Element of NAT st k in Seg(len p)
    holds P[k,f/.k] from RECDEF_1:sch 17(A1);
    take f;
A3: len f = len p by A2,FINSEQ_1:def 3;
    now
      let m be Nat;
      assume 1 <= m & m <= len f;
      then m in Seg(len p) by A3,FINSEQ_1:1;
      hence f/.m = p/.m + q/.m by A2;
    end;
    hence thesis by A2,FINSEQ_1:def 3;
  end;
  uniqueness
  proof
    let y1,y2 be FinSequence of the carrier of R;
    assume that
A4: dom y1 = dom p and
A5: for i being Nat st 1 <= i & i <= len y1 holds y1/.i = p/.i + q/.i and
A6: dom y2 = dom p and
A7: for i being Nat st 1 <= i & i <= len y2 holds y2/.i = p/.i + q/.i;
A8: Seg(len y1) = dom y2 by A4,A6,FINSEQ_1:def 3
      .= Seg(len y2) by FINSEQ_1:def 3;
    then
A9: len y1 = len y2 by FINSEQ_1:6;
    now
      let i be Nat;
      assume
A10:  1 <= i & i <= len y1;
      then i in Seg (len y2) by A8,FINSEQ_1:1;
      then
A11:  i in dom y2 by FINSEQ_1:def 3;
      i in Seg (len y1) by A10,FINSEQ_1:1;
      then i in dom y1 by FINSEQ_1:def 3;
      hence y1.i = y1/.i by PARTFUN1:def 6
        .= p/.i + q/.i by A5,A10
        .= y2/.i by A7,A9,A10
        .= y2.i by A11,PARTFUN1:def 6;
    end;
    hence thesis by A8,FINSEQ_1:6,14;
  end;
end;

theorem Th7:
  for R being Abelian right_zeroed add-associative non empty
  addLoopStr, p,q being FinSequence of the carrier of R st dom p = dom q holds
  Sum(p + q) = Sum p + Sum q
proof
  let R be Abelian right_zeroed add-associative non empty addLoopStr, p,q be
  FinSequence of the carrier of R;
  consider fp being Function of NAT,the carrier of R such that
A1: Sum p = fp.(len p) and
A2: fp.0 = 0.R and
A3: for j being Element of NAT, v being Element of R st j < len p & v =
  p.(j + 1) holds fp.(j + 1) = fp.j + v by RLVECT_1:def 12;
  consider fq being Function of NAT,the carrier of R such that
A4: Sum q = fq.(len q) and
A5: fq.0 = 0.R and
A6: for j being Element of NAT, v being Element of R st j < len q & v =
  q.(j + 1) holds fq.(j + 1) = fq.j + v by RLVECT_1:def 12;
  assume dom p = dom q;
  then
A7: Seg(len p) = dom q by FINSEQ_1:def 3
    .= Seg(len q) by FINSEQ_1:def 3;
  then
A8: len q = len p by FINSEQ_1:6;
  consider fa being Function of NAT,the carrier of R such that
A9: Sum(p+q) = fa.(len(p+q)) and
A10: fa.0 = 0.R and
A11: for j being Element of NAT, v being Element of R st j < len(p+q) &
  v = (p+q).(j + 1) holds fa.(j + 1) = fa.j + v by RLVECT_1:def 12;
  defpred P[Element of NAT] means fp.$1 + fq.$1 = fa.$1;
A12: Seg(len p) = dom p by FINSEQ_1:def 3
    .= dom(p+q) by Def1
    .= Seg(len(p+q)) by FINSEQ_1:def 3;
  then
A13: len(p+q) = len p by FINSEQ_1:6;
A14: now
    let j be Element of NAT;
    assume that
    0 <= j and
A15: j < len p;
    thus P[j] implies P[j+1]
    proof
      assume
A16:  P[j];
A17:  0 + 1 <= j + 1 by XREAL_1:6;
A18:  j + 1 <= len p by A15,NAT_1:13;
      then j + 1 in Seg len p by A17,FINSEQ_1:1;
      then j + 1 in dom p by FINSEQ_1:def 3;
      then
A19:  p/.(j + 1) = p.(j + 1) by PARTFUN1:def 6;
      j + 1 in Seg len q by A7,A18,A17,FINSEQ_1:1;
      then j + 1 in dom q by FINSEQ_1:def 3;
      then
A20:  q/.(j + 1) = q.(j + 1) by PARTFUN1:def 6;
A21:  j + 1 <= len(p+q) by A13,A15,NAT_1:13;
      then j + 1 in Seg len(p+q) by A17,FINSEQ_1:1;
      then j + 1 in dom(p+q) by FINSEQ_1:def 3;
      then (p+q)/.(j + 1) = (p+q).(j + 1) by PARTFUN1:def 6;
      then fa.(j+1) = fa.j + (p+q)/.(j + 1) by A13,A11,A15
        .= (fp.j + fq.j) + (p/.(j + 1) + q/.(j + 1)) by A16,A21,A17,Def1
        .= fp.j + (fq.j + (p/.(j + 1) + q/.(j + 1))) by RLVECT_1:def 3
        .= fp.j + (p/.(j + 1) + (fq.j + q/.(j + 1))) by RLVECT_1:def 3
        .= (fp.j + p/.(j + 1)) + (fq.j + q/.(j + 1)) by RLVECT_1:def 3
        .= fp.(j+1) + (fq.j + q/.(j + 1)) by A3,A15,A19
        .= fp.(j+1) + fq.(j+1) by A8,A6,A15,A20;
      hence thesis;
    end;
  end;
A22: P[0] by A2,A5,A10,RLVECT_1:def 4;
A23: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from
  INT_1:sch 7(A22,A14);
  thus Sum(p + q) = fa.(len p) by A12,A9,FINSEQ_1:6
    .= Sum p + Sum q by A8,A1,A4,A23;
end;

begin  ::  On Powers in Rings

definition
  let R be unital non empty multMagma, a be Element of R, n be Nat;
  func a|^n -> Element of R equals
  power(R).(a,n);
  coherence
  proof
    reconsider n as Element of NAT by ORDINAL1:def 12;
    power(R).(a,n) is Element of R;
    hence thesis;
  end;
end;

theorem Th8:
  for R being unital non empty multMagma, a being Element of R
  holds a|^0 = 1_R & a|^1 = a
proof
  let R be unital non empty multMagma, a be Element of R;
  thus a|^0 = 1_R by GROUP_1:def 7;
  0 + 1 = 1;
  then power(R).(a,1) = power(R).(a,0) * a by GROUP_1:def 7
    .= 1_R * a by GROUP_1:def 7
    .= a by GROUP_1:def 4;
  hence thesis;
end;

theorem
  for R being unital associative commutative non empty multMagma,
  a,b being Element of R, n being Nat holds
  (a * b)|^n = (a|^n) * (b|^n)
proof
  let R be unital associative commutative non empty multMagma, a,b be
  Element of R, n be Nat;
A1:n in NAT by ORDINAL1:def 12;
  defpred P[Element of NAT] means power(R).(a * b,$1) = power(R).(a,$1) *
  power(R).(b,$1);
A2: now
    let m be Element of NAT;
    assume P[m];
    then
    power(R).(a * b,m+1) = (power(R).(a,m) * power(R).(b,m)) * (a * b) by
GROUP_1:def 7
      .= ((power(R).(a,m) * power(R).(b,m)) * a) * b by GROUP_1:def 3
      .= ((power(R).(a,m) * a) * power(R).(b,m)) * b by GROUP_1:def 3
      .= (power(R).(a,m) * a) * (power(R).(b,m) * b) by GROUP_1:def 3
      .= power(R).(a,m+1) * (power(R).(b,m) * b) by GROUP_1:def 7
      .= power(R).(a,m+1) * power(R).(b,m+1) by GROUP_1:def 7;
    hence P[m+1];
  end;
  power(R).(a * b,0) = 1_R by GROUP_1:def 7
    .= 1_R * 1_R by GROUP_1:def 4
    .= power(R).(a,0) * 1_R by GROUP_1:def 7
    .= power(R).(a,0) * power(R).(b,0) by GROUP_1:def 7;
  then
A3: P[0];
  for m being Element of NAT holds P[m] from NAT_1:sch 1(A3,A2);
  hence thesis by A1;
end;

Lm3:
  for R being unital associative non empty multMagma,
  a being Element of R, n,m being Element of NAT holds
  a|^(n+m) = (a|^n) * (a|^m)
proof
  let R be unital associative non empty multMagma, a be Element of R,
  n,m be Element of NAT;
  defpred P[Element of NAT] means power(R).(a,n+$1) =
    power(R).(a,n) * power(R).(a,$1);
A1: now
    let m be Element of NAT;
    assume
A2: P[m];
    power(R).(a,n+(m+1)) = power(R).(a,(n+m)+1)
      .= (power(R).(a,n) * power(R).(a,m)) * a by A2,GROUP_1:def 7
      .= power(R).(a,n) * (power(R).(a,m) * a) by GROUP_1:def 3
      .= power(R).(a,n) * power(R).(a,(m+1)) by GROUP_1:def 7;
    hence P[m+1];
  end;
  power(R).(a,n + 0) = power(R).(a,n) * 1_R by GROUP_1:def 4
    .= power(R).(a,n) * power(R).(a,0) by GROUP_1:def 7;
  then
A3: P[0];
  for m being Element of NAT holds P[m] from NAT_1:sch 1(A3,A1);
  hence thesis;
end;

theorem Th10:
  for R being unital associative non empty multMagma,
  a being Element of R, n,m being Nat holds
  a|^(n+m) = (a|^n) * (a|^m)
proof
  let R be unital associative non empty multMagma, a be Element of R,
  n,m be Nat;
  reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
  a|^(n1+m1) = (a|^n1) * (a|^m1) by Lm3;
  hence thesis;
end;

theorem
  for R being unital associative non empty multMagma, a being Element
  of R, n,m being Nat holds (a|^n)|^m = a|^(n * m)
proof
  let R be unital associative non empty multMagma, a be Element of R, n,m be
  Nat;
A1:n in NAT & m in NAT by ORDINAL1:def 12;
  defpred P[Element of NAT] means power(R).(a|^n,$1) = power(R).(a,n * $1);
A2: now
    let m be Element of NAT;
    assume P[m];
    then power(R).(a|^n,m+1) = a|^(n * m) * (a|^n) by GROUP_1:def 7
      .= a|^(n * m + n) by Th10
      .= power(R).(a,n * (m + 1));
    hence P[m+1];
  end;
  power(R).(a|^n,0) = 1_R by GROUP_1:def 7
    .= power(R).(a,n * 0) by GROUP_1:def 7;
  then
A3: P[0];
  for k being Element of NAT holds P[k] from NAT_1:sch 1(A3,A2);
  hence thesis by A1;
end;

begin :: On Natural Products in Rings

definition
  let R be non empty addLoopStr;
  func Nat-mult-left(R) -> Function of [:NAT,the carrier of R:],the carrier of
  R means
  :Def3:
  for a being Element of R holds it.(0,a) = 0.R & for n being
  Element of NAT holds it.(n+1,a) = a + it.(n,a);
  existence
  proof
    set D = the carrier of R;
    consider g being Function of [:NAT,D:],D such that
A1: for a being Element of D holds g.(0,a) = 0.R & for n being Element
    of NAT holds g.(n+1,a) = (the addF of R).(a,g.(n,a)) by Lm1;
    take g;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let f,g be Function of [:NAT,the carrier of R:],the carrier of R;
    assume
A2: for a being Element of R holds f.(0,a) = 0.R & for n being Element
    of NAT holds f.(n+1,a) = a + f.(n,a);
    defpred P[Element of NAT] means for a being Element of R holds f.($1,a) =
    g.($1,a);
    assume
A3: for a being Element of R holds g.(0,a) = 0.R & for n being Element
    of NAT holds g.(n+1,a) = a + g.(n,a);
A4: now
      let n be Element of NAT;
      assume
A5:   P[n];
      now
        let a be Element of R;
        thus f.(n+1,a) = a + f.(n,a) by A2
          .= a + g.(n,a) by A5
          .= g.(n+1,a) by A3;
      end;
      hence P[n+1];
    end;
A6: P[0]
    proof
      let a be Element of R;
      thus f.(0,a) = 0.R by A2
        .= g.(0,a) by A3;
    end;
A7: for n being Element of NAT holds P[n] from NAT_1:sch 1(A6,A4);
A8: now
      let x be set;
      assume x in [:NAT,the carrier of R:];
      then consider u,v being set such that
A9:   u in NAT and
A10:  v in the carrier of R and
A11:  x = [u,v] by ZFMISC_1:def 2;
      reconsider v as Element of R by A10;
      reconsider u as Element of NAT by A9;
      thus f.x = f.(u,v) by A11
        .= g.(u,v) by A7
        .= g.x by A11;
    end;
    dom f = [:NAT,the carrier of R:] & dom g = [:NAT,the carrier of R:] by
FUNCT_2:def 1;
    hence thesis by A8,FUNCT_1:2;
  end;
  func Nat-mult-right(R) -> Function of [:the carrier of R,NAT:],the carrier
  of R means
  :Def4:
  for a being Element of R holds it.(a,0) = 0.R & for n being
  Element of NAT holds it.(a,n+1) = it.(a,n) + a;
  existence
  proof
    consider g being Function of [:the carrier of R,NAT:],the carrier of R
    such that
A12: for a being Element of R holds g.(a,0) = 0.R & for n being
    Element of NAT holds g.(a,n+1) = (the addF of R).(g.(a,n),a) by Lm2;
    take g;
    thus thesis by A12;
  end;
  uniqueness
  proof
    let f,g be Function of [:the carrier of R,NAT:],the carrier of R;
    assume
A13: for a being Element of R holds f.(a,0) = 0.R & for n being
    Element of NAT holds f.(a,n+1) = f.(a,n) + a;
    defpred P[Element of NAT] means for a being Element of R holds f.(a,$1) =
    g.(a,$1);
    assume
A14: for a being Element of R holds g.(a,0) = 0.R & for n being
    Element of NAT holds g.(a,n+1) = g.(a,n) + a;
A15: now
      let n be Element of NAT;
      assume
A16:  P[n];
      now
        let a be Element of R;
        thus f.(a,n+1) = f.(a,n) + a by A13
          .= g.(a,n) + a by A16
          .= g.(a,n+1) by A14;
      end;
      hence P[n+1];
    end;
A17: P[0]
    proof
      let a be Element of R;
      thus f.(a,0) = 0.R by A13
        .= g.(a,0) by A14;
    end;
A18: for n being Element of NAT holds P[n] from NAT_1:sch 1(A17,A15);
A19: now
      let x be set;
      assume x in [:the carrier of R,NAT:];
      then consider v,u being set such that
A20:  v in the carrier of R and
A21:  u in NAT and
A22:  x = [v,u] by ZFMISC_1:def 2;
      reconsider v as Element of R by A20;
      reconsider u as Element of NAT by A21;
      thus f.x = f.(v,u) by A22
        .= g.(v,u) by A18
        .= g.x by A22;
    end;
    dom f = [:the carrier of R,NAT:] & dom g = [:the carrier of R,NAT:]
    by FUNCT_2:def 1;
    hence thesis by A19,FUNCT_1:2;
  end;
end;

definition
  let R be non empty addLoopStr, a be Element of R, n be Element of NAT;
  func n * a -> Element of R equals
  (Nat-mult-left(R)).(n,a);
  coherence;
  func a * n -> Element of R equals
  (Nat-mult-right(R)).(a,n);
  coherence;
end;

theorem
  for R being non empty addLoopStr, a being Element of R holds 0 * a =
  0.R & a * 0 = 0.R by Def3,Def4;

theorem Th13:
  for R being right_zeroed non empty addLoopStr, a being Element
  of R holds 1 * a = a
proof
  let R be right_zeroed non empty addLoopStr, a be Element of R;
  thus 1 * a = (Nat-mult-left(R)).(0+1,a)
    .= a + (Nat-mult-left(R)).(0,a) by Def3
    .= a + 0.R by Def3
    .= a by RLVECT_1:def 4;
end;

theorem Th14:
  for R being left_zeroed non empty addLoopStr, a being Element
  of R holds a * 1 = a
proof
  let R be left_zeroed non empty addLoopStr, a be Element of R;
  thus a * 1 = (Nat-mult-right(R)).(a,0+1)
    .= (Nat-mult-right(R)).(a,0) + a by Def4
    .= 0.R + a by Def4
    .= a by ALGSTR_1:def 2;
end;

theorem Th15:
  for R being left_zeroed add-associative non empty addLoopStr,
a being Element of R, n,m being Element of NAT holds (n + m) * a = n * a + m *
  a
proof
  let R be left_zeroed add-associative non empty addLoopStr, a be Element of
  R, n,m be Element of NAT;
  defpred P[Element of NAT] means ($1 + m) * a = $1 * a + m * a;
A1: now
    let k be Element of NAT;
    assume
A2: P[k];
    ((k+1) + m) * a = ((k+m) + 1) * a .= a + (k * a + m * a) by A2,Def3
      .= (a + k * a) + m * a by RLVECT_1:def 3
      .= (k+1) * a + m * a by Def3;
    hence P[k+1];
  end;
  (0 + m) * a = 0.R + m * a by ALGSTR_1:def 2
    .= 0 * a + m * a by Def3;
  then
A3: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A3,A1);
  hence thesis;
end;

theorem Th16:
  for R being right_zeroed add-associative non empty addLoopStr,
a being Element of R, n,m being Element of NAT holds a * (n + m) = a * n + a *
  m
proof
  let R be right_zeroed add-associative non empty addLoopStr, a be Element
  of R, n,m be Element of NAT;
  defpred P[Element of NAT] means a * (n + $1) = a * n + a * $1;
A1: now
    let k be Element of NAT;
    assume
A2: P[k];
    a * (n + (k+1)) = a * ((n+k) + 1) .= (a * n + a * k) + a by A2,Def4
      .= a * n + (a * k + a) by RLVECT_1:def 3
      .= a * n + a * (k+1) by Def4;
    hence P[k+1];
  end;
  a * (n + 0) = a * n + 0.R by RLVECT_1:def 4
    .= a * n + a * 0 by Def4;
  then
A3: P[0];
  for m being Element of NAT holds P[m] from NAT_1:sch 1(A3,A1);
  hence thesis;
end;

theorem Th17:
  for R being left_zeroed right_zeroed add-associative non empty
  addLoopStr, a being Element of R, n being Element of NAT holds n * a = a * n
proof
  let R be left_zeroed right_zeroed add-associative non empty addLoopStr, a
  be Element of R, n be Element of NAT;
  defpred P[Element of NAT] means $1 * a = a * $1;
A1: now
    let k be Element of NAT;
    assume
A2: P[k];
    (k + 1) * a = k * a + 1 * a by Th15
      .= k * a + a by Th13
      .= a * k + a * 1 by A2,Th14
      .= a * (k + 1) by Th16;
    hence P[k+1];
  end;
  0 * a = 0.R by Def3
    .= a * 0 by Def4;
  then
A3: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A3,A1);
  hence thesis;
end;

theorem
  for R being Abelian non empty addLoopStr, a being Element of R, n
  being Element of NAT holds n * a = a * n
proof
  let R be Abelian non empty addLoopStr, a be Element of R, n be Element of
  NAT;
  defpred P[Element of NAT] means $1 * a = a * $1;
A1: now
    let k be Element of NAT;
    assume P[k];
    then (k + 1) * a = a + a * k by Def3
      .= a * (k + 1) by Def4;
    hence P[k+1];
  end;
  0 * a = 0.R by Def3
    .= a * 0 by Def4;
  then
A2: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A2,A1);
  hence thesis;
end;

theorem Th19:
  for R being left_zeroed right_zeroed left_add-cancelable
add-associative left-distributive non empty doubleLoopStr, a,b being Element
  of R, n being Element of NAT holds (n * a) * b = n * (a * b)
proof
  let R be left_zeroed right_zeroed left_add-cancelable add-associative
left-distributive non empty doubleLoopStr, a,b be Element of R, n be Element
  of NAT;
  defpred P[Element of NAT] means ($1 * a) * b = $1 * (a * b);
A1: now
    let k be Element of NAT;
    assume
A2: P[k];
    ((k+1) * a) * b = (a + k * a) * b by Def3
      .= a * b + k * (a * b) by A2,VECTSP_1:def 3
      .= 1 * (a * b) + k * (a * b) by Th13
      .= (k + 1) * (a * b) by Th15;
    hence P[k+1];
  end;
  (0 * a) * b = 0.R * b by Def3
    .= 0.R by Th1
    .= 0 * (a * b) by Def3;
  then
A3: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A3,A1);
  hence thesis;
end;

theorem Th20:
  for R being left_zeroed right_zeroed right_add-cancelable
add-associative distributive non empty doubleLoopStr, a,b being Element of R,
  n being Element of NAT holds b * (n * a) = (b * a) * n
proof
  let R be left_zeroed right_zeroed add-associative right_add-cancelable
  distributive non empty doubleLoopStr, a,b be Element of R, n be Element of
  NAT;
  defpred P[Element of NAT] means b * ($1 * a) = (b * a) * $1;
A1: now
    let k be Element of NAT;
    assume
A2: P[k];
    b * ((k+1)* a) = b * (a + k * a) by Def3
      .= b * a + (b * a) * k by A2,VECTSP_1:def 2
      .= (b * a) * 1 + (b * a) * k by Th14
      .= (b * a) * (k + 1) by Th16;
    hence P[k+1];
  end;
  b * (0 * a) = b * 0.R by Def3
    .= 0.R by Th2
    .= (b * a) * 0 by Def4;
  then
A3: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A3,A1);
  hence thesis;
end;

theorem Th21:
  for R being left_zeroed right_zeroed add-associative
add-cancelable distributive non empty doubleLoopStr, a,b being Element of R,
  n being Element of NAT holds (a * n) * b = a * (n * b)
proof
  let R be left_zeroed right_zeroed distributive add-cancelable
add-associative non empty doubleLoopStr, a,b be Element of R, n be Element of
  NAT;
  thus (a * n) * b = (n * a) * b by Th17
    .= n * (a * b) by Th19
    .= (a * b) * n by Th17
    .= a * (n * b) by Th20;
end;

begin  ::  The Binomial Theorem

definition
  let k,n be Element of NAT;
  redefine func n choose k -> Element of NAT;
  coherence by NEWTON:25;
end;

definition
  let R be unital non empty doubleLoopStr, a,b be Element of R, n be Element
  of NAT;
  func (a,b) In_Power n -> FinSequence of the carrier of R means
  :Def7:
  len
it = n + 1 & for i,l,m being Element of NAT st i in dom it & m = i - 1 & l = n
  - m holds it/.i = (n choose m) * a|^l * b|^m;
  existence
  proof
    defpred P[Element of NAT,Element of R] means for l,m being Element of NAT
    st m = $1 - 1 & l = n - m holds $2 = (n choose m) * a|^l * b|^m;
A1: for k being Element of NAT st k in Seg(n+1) ex y being Element of R st
    P[k,y]
    proof
      let k be Element of NAT;
      assume
A2:   k in Seg(n+1);
      then k >= 1 by FINSEQ_1:1;
      then reconsider m1 = k-1 as Element of NAT by INT_1:5;
      k <= n+1 by A2,FINSEQ_1:1;
      then k-1<=n+1-1 by XREAL_1:9;
      then reconsider l1 = n-m1 as Element of NAT by INT_1:5;
      reconsider z = (n choose m1) * a|^l1 * b|^m1 as Element of R;
      take z;
      thus thesis;
    end;
    consider p being FinSequence of the carrier of R such that
A3: dom p = Seg(n+1) & for k being Element of NAT st k in Seg(n+1)
    holds P[k,p/.k] from RECDEF_1:sch 17(A1);
    take p;
    thus thesis by A3,FINSEQ_1:def 3;
  end;
  uniqueness
  proof
    let f,g be FinSequence of the carrier of R;
    assume that
A4: len f = n + 1 and
A5: for i,l,m being Element of NAT st i in dom f & m = i - 1 & l = n -
    m holds f/.i = (n choose m) * a|^l * b|^m;
    assume that
A6: len g = n + 1 and
A7: for i,l,m being Element of NAT st i in dom g & m = i - 1 & l = n
    - m holds g/.i = (n choose m) * a|^l * b|^m;
    for i being Nat st 1 <= i & i <= len f holds f.i = g.i
    proof
      let i be Nat;
      assume that
A8:   1 <= i and
A9:   i <= len f;
      reconsider m = i-1 as Element of NAT by A8,INT_1:5;
      i-1<=n+1-1 by A4,A9,XREAL_1:9;
      then reconsider l = n-m as Element of NAT by INT_1:5;
A10:  i in Seg (n+1) by A4,A8,A9,FINSEQ_1:1;
      then
A11:  i in dom f by A4,FINSEQ_1:def 3;
A12:  i in dom g by A6,A10,FINSEQ_1:def 3;
      hence g.i = g/.i by PARTFUN1:def 6
        .= (n choose m) * a|^l * b|^m by A7,A12
        .= f/.i by A5,A11
        .= f.i by A11,PARTFUN1:def 6;
    end;
    hence f = g by A4,A6,FINSEQ_1:14;
  end;
end;

theorem Th22:
  for R being right_zeroed unital non empty doubleLoopStr, a,b
  being Element of R holds (a,b) In_Power 0 = <*1_R*>
proof
  let R be right_zeroed unital non empty doubleLoopStr, a,b being Element of
  R;
  set p = (a,b) In_Power 0;
A1: len p = 0 + 1 by Def7
    .= 1;
  then
A2: dom p = {1} by FINSEQ_1:2,def 3;
  then
A3: 1 in dom p by TARSKI:def 1;
  then consider i being Element of NAT such that
A4: i in dom p;
A5: i = 1 by A2,A4,TARSKI:def 1;
  then reconsider m = i - 1 as Element of NAT by INT_1:5;
  reconsider l = 0 - m as Element of NAT by A5;
  p.1 = p/.1 by A3,PARTFUN1:def 6
    .= (0 choose m) * a|^l * b|^m by A3,A5,Def7
    .= 1 * a|^l * b|^m by A5,NEWTON:19
    .= 1 * a|^0 * 1_R by A5,Th8
    .= 1 * 1_R * 1_R by Th8
    .= 1_R * 1_R by Th13
    .= 1_R by GROUP_1:def 4;
  hence thesis by A1,FINSEQ_1:40;
end;

theorem Th23:
  for R being right_zeroed unital non empty doubleLoopStr, a,b
  being Element of R, n being Element of NAT holds ((a,b) In_Power n).1 = a|^n
proof
  reconsider m = 1 - 1 as Element of NAT by NEWTON:19;
  let R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R,
  n be Element of NAT;
  reconsider l = n - m as Element of NAT;
  len((a,b) In_Power n) = n + 1 by Def7;
  then
A1: dom(((a,b) In_Power n)) = Seg(n + 1) by FINSEQ_1:def 3;
  0 + 1 <= n + 1 by XREAL_1:6;
  then
A2: 1 in dom(((a,b) In_Power n)) by A1,FINSEQ_1:1;
  hence ((a,b) In_Power n).1 = ((a,b) In_Power n)/.1 by PARTFUN1:def 6
    .= (n choose 0) * a|^l * b|^m by A2,Def7
    .= 1 * a|^n * b|^0 by NEWTON:19
    .= a|^n * b|^0 by Th13
    .= a|^n * 1_R by Th8
    .= a|^n by GROUP_1:def 4;
end;

theorem Th24:
  for R being right_zeroed unital non empty doubleLoopStr, a,b
being Element of R, n being Element of NAT holds ((a,b) In_Power n).(n+1) = b|^
  n
proof
  let R be right_zeroed unital non empty doubleLoopStr, a,b be Element of R,
  n be Element of NAT;
  reconsider m = n + 1 - 1 as Element of NAT;
  reconsider l = n - m as Element of NAT by INT_1:5;
  len((a,b) In_Power n) = n + 1 by Def7;
  then
A1: dom((a,b) In_Power n) = Seg(n + 1) by FINSEQ_1:def 3;
  then
A2: l = 0 & n + 1 in dom((a,b) In_Power n) by FINSEQ_1:4;
  thus ((a,b) In_Power n).(n+1) = ((a,b) In_Power n)/.(n+1) by A1,FINSEQ_1:4
,PARTFUN1:def 6
    .= (n choose n) * a|^0 * b|^n by A2,Def7
    .= 1 * a|^0 * b|^n by NEWTON:21
    .= 1 * 1_R * b|^n by Th8
    .= 1_R * b|^n by Th13
    .= b|^n by GROUP_1:def 4;
end;

::$N Binomial Theorem
theorem
  for R being Abelian add-associative left_zeroed right_zeroed
  commutative associative add-cancelable distributive unital non empty
doubleLoopStr, a,b being Element of R, n being Element of NAT holds (a+b)|^n =
  Sum((a,b) In_Power n)
proof
  let R be add-associative left_zeroed right_zeroed distributive associative
  Abelian add-cancelable commutative unital non empty doubleLoopStr, a,b be
  Element of R, n be Element of NAT;
  defpred P[Element of NAT] means (a+b)|^$1 = Sum((a,b) In_Power $1);
A1: for n being Element of NAT st P[n] holds P[n+1]
  proof
    let n be Element of NAT;
    set G1 = (((a,b) In_Power n) * a)^<*0.R*>;
    set G2 = <*0.R*>^(((a,b) In_Power n) * b);
A2: Seg(len(((a,b) In_Power n) * a)) = dom(((a,b) In_Power n) * a) by
FINSEQ_1:def 3
      .= dom((a,b) In_Power n) by POLYNOM1:def 2
      .= Seg(len((a,b) In_Power n)) by FINSEQ_1:def 3;
    len G1 = len(((a,b) In_Power n) * a) + len<*0.R*> by FINSEQ_1:22
      .= len(((a,b) In_Power n) * a) + 1 by FINSEQ_1:40
      .= len((a,b) In_Power n) + 1 by A2,FINSEQ_1:6
      .= n + 1 + 1 by Def7;
    then reconsider
    F1 = G1 as Element of (n+1+1)-tuples_on the carrier of R by FINSEQ_2:92;
A3: Seg(len(((a,b) In_Power n) * b)) = dom(((a,b) In_Power n) * b) by
FINSEQ_1:def 3
      .= dom((a,b) In_Power n) by POLYNOM1:def 2
      .= Seg(len((a,b) In_Power n)) by FINSEQ_1:def 3;
    len G2 = len(((a,b) In_Power n) * b) + len<*0.R*> by FINSEQ_1:22
      .= len(((a,b) In_Power n) * b) + 1 by FINSEQ_1:40
      .= len((a,b) In_Power n) + 1 by A3,FINSEQ_1:6
      .= n + 1 + 1 by Def7;
    then reconsider
    F2 = G2 as Element of (n+1+1)-tuples_on the carrier of R by FINSEQ_2:92;
A4: len F1 = n+1+1 by CARD_1:def 7;
    set F = F1 + F2;
A5: len F2 = n+1+1 by CARD_1:def 7;
A6: Seg(len F) = dom F by FINSEQ_1:def 3
      .= dom F1 by Def1
      .= Seg(len F1) by FINSEQ_1:def 3;
    then
A7: len F = n + 1 + 1 by A4,FINSEQ_1:6;
A8: for i being Nat st 1 <= i & i <= len((a,b) In_Power (n+1)) holds F.i
    = ((a,b) In_Power (n+1)).i
    proof
      let i be Nat;
      assume that
A9:   1 <= i and
A10:  i <= len((a,b) In_Power (n+1));
A11:  len((a,b) In_Power (n+1)) = n+1+1 by Def7;
      then
A12:  dom((a,b) In_Power (n+1)) = Seg(n+1+1) by FINSEQ_1:def 3;
      then
A13:  i in dom((a,b) In_Power (n+1)) by A9,A10,A11,FINSEQ_1:1;
      reconsider j = i - 1 as Element of NAT by A9,INT_1:5;
      set x = ((a,b) In_Power n)/.j;
      set r1 = F1/.i;
      set r2 = F2/.i;
      set r = ((a,b) In_Power n)/.i;
A14:  i = j+1;
A15:  i in Seg(n+1+1) by A9,A10,A11,FINSEQ_1:1;
      then
A16:  i in dom F1 by A4,FINSEQ_1:def 3;
A17:  i in dom F2 by A5,A15,FINSEQ_1:def 3;
A18:  i <= len(F1+F2) by A7,A10,Def7;
A19:  i in {n+1+1} implies F.i = ((a,b) In_Power (n+1)).i
      proof
        assume
A20:    i in {n+1+1};
        then
A21:    i = n+1+1 by TARSKI:def 1;
        n+1 = len ((a,b) In_Power n) by Def7
          .= len(((a,b) In_Power n) * a) by A2,FINSEQ_1:6;
        then
A22:    r1 = ((((a,b) In_Power n)*a)^<*0.R*>). (len(((a,b) In_Power n)*a)
        +1) by A16,A21,PARTFUN1:def 6
          .= 0.R by FINSEQ_1:42;
A23:    j = n+1+1-1 by A20,TARSKI:def 1
          .= n+1;
        n+1 in Seg (n+1) by FINSEQ_1:4;
        then
A24:    j in Seg len (((a,b) In_Power n)) by A23,Def7;
        then
A25:    j in dom (((a,b) In_Power n) * b) by A3,FINSEQ_1:def 3;
A26:    j in dom ((a,b) In_Power n) by A24,FINSEQ_1:def 3;
        then
A27:    x = ((a,b) In_Power n).(n+1) by A23,PARTFUN1:def 6
          .= b|^n by Th24;
A28:    r2 = (<*0.R*>^(((a,b) In_Power n) * b)).(1+(n+1)) by A17,A21,
PARTFUN1:def 6
          .= (<*0.R*>^(((a,b) In_Power n) * b)).(len <*0.R*> + j) by A23,
FINSEQ_1:39
          .= (((a,b) In_Power n) * b).j by A25,FINSEQ_1:def 7
          .= (((a,b) In_Power n) * b)/.j by A25,PARTFUN1:def 6
          .= b|^n * b by A26,A27,POLYNOM1:def 2
          .= b|^(n+1) by GROUP_1:def 7;
        dom F = Seg(n+1+1) by A4,A6,FINSEQ_1:def 3;
        then i in dom F by A9,A21,FINSEQ_1:1;
        hence F.i = F/.i by PARTFUN1:def 6
          .= 0.R + r2 by A9,A18,A22,Def1
          .= b|^(n+1) by A28,ALGSTR_1:def 2
          .= ((a,b) In_Power (n+1)).i by A21,Th24;
      end;
A29:  i in dom F by A4,A6,A15,FINSEQ_1:def 3;
A30:  i in {k where k is Element of NAT: k>1 & k<n+1+1} implies F.i = ((a
      ,b) In_Power (n+1)).i
      proof
        assume i in {k where k is Element of NAT: 1 < k & k < n+1+1};
        then
A31:    ex k being Element of NAT st k = i & 1 < k & k < n+1+1;
        then reconsider m1 = i-1 as Element of NAT by INT_1:5;
A32:    i <= n+1 by A31,NAT_1:13;
        then i in Seg (n+1) by A31,FINSEQ_1:1;
        then
A33:    i in Seg len ((a,b) In_Power n) by Def7;
        then
A34:    i in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
        1 <= j by A14,A31,NAT_1:13;
        then reconsider m2 = j - 1 as Element of NAT by INT_1:5;
A35:    j <= n+1 by A14,A31,XREAL_1:6;
        then j-1<=n+1-1 by XREAL_1:9;
        then reconsider l2 = n-m2 as Element of NAT by INT_1:5;
        1 <= j by A14,A31,NAT_1:13;
        then j in Seg (n+1) by A35,FINSEQ_1:1;
        then
A36:    j in Seg len ((a,b) In_Power n) by Def7;
        then
A37:    j in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
A38:    j in dom (((a,b) In_Power n) * b) by A3,A36,FINSEQ_1:def 3;
A39:    j in dom (((a,b) In_Power n) * b) by A3,A36,FINSEQ_1:def 3;
        r2=(<*0.R*>^(((a,b) In_Power n)*b)).i by A17,PARTFUN1:def 6;
        then
A40:    r2 = (<*0.R*>^(((a,b) In_Power n) * b)).(len <*0.R*> +j) by A14,
FINSEQ_1:40
          .= (((a,b) In_Power n) * b).j by A39,FINSEQ_1:def 7
          .= (((a,b) In_Power n) * b)/.j by A38,PARTFUN1:def 6
          .= x * b by A37,POLYNOM1:def 2;
        i-1 <= n+1-1 by A32,XREAL_1:9;
        then reconsider l1 = n - m1 as Element of NAT by INT_1:5;
A41:    l1+1 = n+1-(m2+1);
A42:    i in dom (((a,b) In_Power n) * a) by A2,A33,FINSEQ_1:def 3;
        r1=((((a,b) In_Power n)*a)^<*0.R*>).i by A16,PARTFUN1:def 6;
        then
A43:    r1 = (((a,b) In_Power n) * a).i by A42,FINSEQ_1:def 7
          .= (((a,b) In_Power n) * a)/.i by A42,PARTFUN1:def 6
          .= r * a by A34,POLYNOM1:def 2;
        thus F.i = F/.i by A29,PARTFUN1:def 6
          .= F1/.i + x * b by A9,A18,A40,Def1
          .= ((n choose m1) * a|^l1 * b|^m1) * a + x * b by A34,A43,Def7
          .= (a|^l1 * (n choose m1) * b|^m1) * a + x * b by Th17
          .= a * (a|^l1 *((n choose m1) * b|^m1)) + x * b by Th21
          .= a * a|^l1 *((n choose m1) * b|^m1) + x * b by GROUP_1:def 3
          .= a|^(l1+1) * ((n choose m1) * b|^m1) + x * b by GROUP_1:def 7
          .= a|^(l1+1) * ((n choose m1) * b|^m1) + b|^m2 * ((n choose m2) *
        a|^l2) * b by A37,Def7
          .= a|^(l1+1) * ((n choose m1) * b|^m1) + (b|^m2 * b) * ((n choose
        m2) * a|^l2) by GROUP_1:def 3
          .= a|^(l1+1) * ((n choose (m2+1)) * b|^(m2+1)) + b|^(m2+1) * ((n
        choose m2) * a|^l2) by GROUP_1:def 7
          .= (b|^(m2+1) * a|^(l1+1)) * (n choose (m2+1)) + b|^(m2+1) * ((n
        choose m2) * a|^l2) by Th20
          .= b|^(m2+1) * ((n choose (m2+1)) * a|^(l1+1)) + b|^(m2+1) * ((n
        choose m2) * a|^l2) by Th20
          .= b|^(m2+1) * (a|^(l1+1) * (n choose (m2+1))) + b|^(m2+1) * ((n
        choose m2) * a|^l2) by Th17
          .= ((a|^(l1+1) * (n choose (m2+1))) + ((n choose m2) * a|^l2)) * b
        |^(m2+1) by VECTSP_1:def 7
          .= (((n choose (m2+1)) * a|^(l1+1)) + ((n choose m2) * a|^(l1+1)))
        * b|^(m2+1) by Th17
          .= ((n choose (m2+1)) + (n choose m2)) * a|^(l1+1) * b|^(m2+1) by
Th15
          .= ((n+1) choose (m2+1)) * a|^(l1+1) * b|^(m2+1) by NEWTON:22
          .= ((a,b) In_Power (n+1))/.i by A13,A41,Def7
          .= ((a,b) In_Power (n+1)).i by A13,PARTFUN1:def 6;
      end;
A44:  i in {1} implies F.i = ((a,b) In_Power (n+1)).i
      proof
        assume i in {1};
        then
A45:    i = 1 by TARSKI:def 1;
        then
A46:    r2 = (<*0.R*>^(((a,b) In_Power n) * b)).1 by A17,PARTFUN1:def 6
          .= 0.R by FINSEQ_1:41;
        n+1 >= 0+1 by XREAL_1:6;
        then 1 in Seg (n+1) by FINSEQ_1:1;
        then
A47:    1 in Seg len(((a,b) In_Power n)) by Def7;
        then
A48:    1 in dom ((a,b) In_Power n) by FINSEQ_1:def 3;
        then
A49:    r = ((a,b) In_Power n).i by A45,PARTFUN1:def 6;
A50:    1 in dom (((a,b) In_Power n) * a) by A2,A47,FINSEQ_1:def 3;
A51:    r1 = ((((a,b) In_Power n) * a)^<*0.R*>).1 by A16,A45,PARTFUN1:def 6
          .= (((a,b) In_Power n) * a).1 by A50,FINSEQ_1:def 7
          .= (((a,b) In_Power n) * a)/.1 by A50,PARTFUN1:def 6
          .= (((a,b) In_Power n)/.1) * a by A48,POLYNOM1:def 2
          .= a|^n * a by A45,A49,Th23
          .= a|^(n+1) by GROUP_1:def 7;
        thus F.i = F/.i by A29,PARTFUN1:def 6
          .= r1 + F2/.i by A9,A18,Def1
          .= a|^(n+1) by A51,A46,RLVECT_1:def 4
          .= ((a,b) In_Power (n+1)).i by A45,Th23;
      end;
      now
        assume
        i in {1} \/ {k where k is Element of NAT: 1<k & k<n+1+1} \/ { n+1+1};
        then i in {1} \/ {k where k is Element of NAT: 1<k & k<n+1+1} or i in
        {n+1+1} by XBOOLE_0:def 3;
        hence thesis by A44,A19,A30,XBOOLE_0:def 3;
      end;
      hence thesis by A12,A13,NAT_1:12,NEWTON:1;
    end;
    assume P[n];
    then
A52: (a+b)|^(n+1) = Sum((a,b) In_Power n) * (a + b) by GROUP_1:def 7
      .= Sum((a,b) In_Power n) * a + Sum ((a,b) In_Power n) * b by
VECTSP_1:def 2
      .= Sum(((a,b) In_Power n) * a) + Sum((a,b) In_Power n) * b by Th5
      .= Sum(((a,b) In_Power n) * a) + Sum(((a,b) In_Power n) * b)by Th5;
A53: Sum F1 = Sum(((a,b) In_Power n) * a) + Sum<*0.R*> by RLVECT_1:41
      .= Sum(((a,b) In_Power n) * a) + 0.R by Th3
      .= Sum(((a,b) In_Power n) * a) by RLVECT_1:def 4;
A54: Sum F2 = Sum<*0.R*> + Sum(((a,b) In_Power n) * b) by RLVECT_1:41
      .= 0.R + Sum(((a,b) In_Power n) * b) by Th3
      .= Sum(((a,b) In_Power n) * b) by ALGSTR_1:def 2;
    dom F1 = Seg(len F1) by FINSEQ_1:def 3
      .= dom F2 by A4,A5,FINSEQ_1:def 3;
    then
A55: Sum(G1+G2) = Sum(((a,b) In_Power n) * a) + Sum (((a,b) In_Power n ) *
    b) by A53,A54,Th7;
    len ((a,b) In_Power (n+1)) = len F by A7,Def7;
    hence thesis by A52,A55,A8,FINSEQ_1:14;
  end;
  (a+b)|^0 = 1_R by Th8
    .= Sum <*1_R*> by Th3
    .= Sum((a,b) In_Power 0) by Th22;
  then
A56: P[0];
  for n being Element of NAT holds P[n] from NAT_1:sch 1(A56,A1);
  hence thesis;
end;

theorem
  for C,D be non empty set, b be Element of D, F be Function of [:C,D:],D
  ex g being Function of [:NAT,C:],D st for a being Element of C holds
  g.(0,a) = b & for n being Element of NAT holds g.(n+1,a) = F.(a,g.(n,a))
  by Lm1;

theorem
  for C,D be non empty set, b be Element of D, F be Function of [:D,C:],D
  ex g being Function of [:C,NAT:],D st for a being Element of C holds
  g.(a,0) = b & for n being Element of NAT holds g.(a,n+1) = F.(g.(a,n),a)
  by Lm2;