UWB Informatyka - Nieoficjalne Forum Studentów

::--------------------------------------------------------------------
::1) scheme s1 { P[Nat] } : for n holds P[n]
::2) scheme s2 { P[Nat] } : for n holds P[n]
::3) scheme s3 { P[Nat] } : for n holds P[n]
::4) scheme s4 { P[Nat] } : for n st n >=1 holds P[n]
::5) scheme s5 { k() -> Nat, P[Nat] } : for n holds P[n]
::6) 1+2+3+...+n = n* (n+1)/2
::7) 1^2 + 2^2 + 3^2 + ... + n^2 = n*(n+1)*(2*n+1)/6
::8) 2 divides n*(n+1)
::9) 6 divides n|^3-n
::10) 2 divides n*(n-1)
::11) 3 divides 10|^n + 4|^n - 2
::12) 9 divides 10|^n -1
::13) 9 divides 4|^n +15*n -1
::14) 6 divides n|^3 + 5*n
::15) n*n >= n
::16) 2|^n >= n
::17) ?
::18) ?
::19) scheme Sch2{P[Nat],m()->Nat}:
::20) scheme Sch3{P[Nat],m()->Nat}:
::21) 2 divides n*(n+1)
::22) 3 divides n*(n+1)*(n+2)
::23) 3 divides 4|^n+5
::24) n|^3=n*n*n
::25) (n+1)|^3=(n+1)*(n+1)*(n+1)
::26) 1 + 3 + 5 + ... + (n-1) = n^2
::27) ex f st f.0=0 & f.1=0 & for n st n>=2 holds f.n=1-1/n
::28) n|^2=n*n
::29) n<>3 &n<>4 implies n|^2<=2|^n
::30) scheme Sch1{P[Nat]}:
::31) scheme Sch2{P[Nat]}:
::32) scheme Sch3 {P[Nat]}:
::33) scheme sch3 {P[Nat]}:
::34) n >= 1 implies ex i,j st n = (2|^i) * (2*j+1)
::35) <a>|1 = <a>
::36) <a>=<a>^<b>
::37) F^<a>^<b>=F^(<a>^<b>)
::38) for f st for i st 1 <= i & i <= len f holds f.i = i holds Sum f = (len f)*(len f+1)/2
::39) ?
::40) (...) holds Sum f = (len f)*(len f)
::41) scheme Sch1{ P[Nat] } : for n holds P[n]
::42) (...) holds f.i = 2*i+1 holds (...) holds Partial_Sums(f).n = (n+1)*(n+1)
::43) 2 divides (n+1)*(n+2)
::44) (...) holds Sum f = (len f)*(len f + 1)/2
::45) 1+2+3+ ... + n = n*(n+1)/2
::56) 1^2+2^2+...+n^2 = n*(n+1)*(2*n+1)/6
::47) 1 + 3 + 5 + ... + (2*n-1) = n*n = n|^2
::48) 1^3 + 2^3 + 3^3 + ... + n^3 = n|^2 * (n+1)|^2 / 4
::49) (...) holds Product f = (len f)!

::--------------------------------------------------------------------
::  1

scheme s1 { P[Nat] } : for n holds P[n]
provided
  z1: P[0] and
  z2: P[1] and
  z3: for n st P[n] holds P[n+2]
proof
  defpred Q[Nat] means P[$1] & P[$1+1];
  a1: Q[0] by z1,z2;
  a2: for n st Q[n] holds Q[n+1]
  proof
    let n such that x1: Q[n];
    P[n] & P[n+1] by x1;
    then P[n+1] & P[n+2] by z3;
    hence Q[n+1];
  end;
  for n holds Q[n] from NAT_1:sch 2 (a1,a2);
  hence for n holds P[n];
end;

::--------------------------------------------------------------------
::  2

scheme s2 { P[Nat] } : for n holds P[n]
provided
  z1: P[0] and
  z2: P[1] and
  z3: P[2] and
  z4: for n st P[n] holds P[n+3]
proof
  defpred Q[Nat] means P[$1] & P[$1+1] & P[$1+2];
  a1: Q[0] by z1,z2,z3;
  a2: for n st Q[n] holds Q[n+1]
  proof
    let n such that x1: Q[n];
    P[n] & P[n+1] & P[n+2] by x1;
    then P[n+1] & P[n+2] & P[n+3] by z4;
    hence Q[n+1];
  end;
  for n holds Q[n] from NAT_1:sch 2 (a1,a2);
  hence for n holds P[n];
end;
::--------------------------------------------------------------------
:: 3
scheme s3 { P[Nat] } : for n holds P[n]
provided
  z1: P[0] and
  z2: P[1] and
  z3: P[2] and
  z4: P[3] and
  z5: for n st P[n] holds P[n+4]
proof
  defpred Q[Nat] means P[$1] & P[$1+1] & P[$1+2] & P[$1+3];
  a1: Q[0] by z1,z2,z3,z4;
  a2: for n st Q[n] holds Q[n+1]
  proof
    let n such that x1: Q[n];
    P[n] & P[n+1] & P[n+2] & P[n+3] by x1;
    then P[n+1] & P[n+2] & P[n+3] & P[n+4] by z5;
    hence Q[n+1];
  end;
  for n holds Q[n] from NAT_1:sch 2 (a1,a2);
  hence for n holds P[n];
end;

::--------------------------------------------------------------------
:: 4

scheme s4 { P[Nat] } : for n st n >=1 holds P[n]
provided
  z1: P[1] and
  z2: for n st n>=1 holds P[n] implies P[n+1]
proof
  defpred Q[Nat] means $1>=1 implies P[$1];
  a1: Q[0];
  a2: for n st Q[n] holds Q[n+1]
  proof
    let n such that x1: Q[n];
    r1: n>=1 implies P[n] by x1;
    thus Q[n+1]
    proof
      assume n+1>=1;
      then n=0 or n>=0+1 by INT_1:20;
      hence P[n+1] by r1,z1,z2;
    end;
  end;
  for n holds Q[n] from NAT_1:sch 2 (a1,a2);
  hence for n st n >=1 holds P[n];
end;

::--------------------------------------------------------------------
:: 5

scheme s5 { k() -> Nat, P[Nat] } : for n holds P[n]
provided
  z1: for n st n<k() holds P[n] and
  z2: for n st P[n] holds P[n+k()] and
  z3: k()>0
proof
  defpred Q[Nat] means for i st i<k() holds P[$1+i];
  a1: Q[0] by z1;
  a2: Q[n] implies Q[n+1]
  proof
    assume Q[n];
    then a3: for i st i<k() holds P[n+i];
    Q[n+1]
    proof
      let i such that X: i <k();
      i+1<=k() by X, INT_1:20;
      then i <=k()-1 by XREAL_1:21;
      then A1: i = k()-1 or i < k()-1 by XXREAL_0: 1;
      per cases by A1;
      suppose S1: i = k()-1;
        then P[n+0] by a3,z3;
        then P[n+k()] by z2;
        hence P[n+1+i] by S1;
      end;
      suppose S2:i < k()-1;
        then i+1 < k() by XREAL_1:22;
        then P[n+(1+i)] by a3;
        hence P[n+1+i];
      end;
    end;
    hence thesis;
  end;
  e: for n holds Q[n] from NAT_1: sch 2(a1,a2);
  let n;
  Q[n] by e;
  then P[n+0] by z3;
  hence thesis;
end;

::--------------------------------------------------------------------
:: 6

:: 1+2+3+...+n = n* (n+1)/2
theorem :: cw1
  for f being Real_Sequence st
  for i being Nat holds f.i = i holds
  for n being Nat holds Partial_Sums(f).n = n*(n+1)/2
proof
  let f being Real_Sequence such that
  a1: for i being Nat holds f.i = i;
  defpred Q[Nat] means Partial_Sums(f).$1 = $1*($1+1)/2;
  p1: Q[0]
  proof
    Partial_Sums(f).0 = f.0 by SERIES_1: def 1
    .= 0 by a1;
::    .= 0*(0+1)/2;
    hence thesis;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that z1: Q[n];
    reconsider n1=n as Element of NAT by ORDINAL1: def 13;
    Partial_Sums(f).(n+1) = Partial_Sums(f).n1 + f.(n+1) by SERIES_1: def 1
    .= n*(n+1)/2 + (n+1) by z1,a1;
::    .= (n+1) * (n+2)/2;
    hence thesis;
  end;
  for n holds Q[n] from NAT_1: sch 2 (p1,p2);
:: hence for n being Nat holds Partial_Sums(f).n = n*(n+1)/2;
  hence thesis;
end;

::--------------------------------------------------------------------
:: 7

:: 1^2 + 2^2 + 3^2 + ... + n^2 = n*(n+1)*(2*n+1)/6
theorem
  for f being Real_Sequence st
  for i being Element of NAT holds f.i = i|^2 holds
  for n being Element of NAT holds Partial_Sums(f).n = n*(n+1)*(2*n+1)/6
proof
  let f being Real_Sequence such that
  a1: for i being Element of NAT holds f.i = i|^2;
  defpred Q[Nat] means Partial_Sums(f).$1 = $1*($1+1)*(2*$1+1)/6;
  p1: Q[0]
  proof
    Partial_Sums(f).0 = f.0 by SERIES_1: def 1
    .= 0|^2 by a1;
::    .= 0*(0+1)*(2*0+1)/6 by NEWTON:16;
    hence thesis by NEWTON:16;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that z1: Q[n];
    z2: (n+1)|^2 = (n+1)|^(1+1) .= (n+1)|^1*(n+1) by NEWTON: 11;
    reconsider n1=n as Element of NAT by ORDINAL1: def 13;
    Partial_Sums(f).(n+1) = Partial_Sums(f).n1 + f.(n+1) by SERIES_1: def 1
    .= n*(n+1)*(2*n+1)/6 + (n+1)|^2 by z1,a1
    .= n*(n+1)*(2*n+1)/6 + (n+1)*(n+1) by z2, NEWTON: 10;
    hence thesis;
  end;
  for n holds Q[n] from NAT_1: sch 2 (p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 8

Th1: 2 divides n*(n+1)
proof
  defpred Q[Nat] means 2 divides $1*($1+1);
  p1: Q[0]
  proof
    0*(0+1) = 2*0;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    consider i being Integer such that z: n*(n+1) = 2*i by a1,INT_1:def 9;
    (n+1)*(n+2)=n*(n+1) + 2*(n+1)
    .= 2*i + 2*(n+1) by z
    .= 2*(i+(n+1));
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 9

6 divides n|^3-n
proof
  defpred Q[Nat] means 6 divides $1|^3-$1;
  p1: Q[0]
  proof
    0|^3-0 = 6*0 by NEWTON: 16;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    s: 1|^3 = 1 & 1|^2 =1 by NEWTON: 15;
    s2: n|^2 = n|^(1+1) .= n*n|^1 by NEWTON:11 .=n*n by NEWTON:10;
    s3: 2 divides n*(n+1) by Th1;
    consider j being Integer such that s4: n*(n+1) = 2*j by s3,INT_1:def 9;
    consider i being Integer such that z: n|^3-n = 6*i by a1,INT_1:def 9;
    (n+1)|^3-(n+1) = n|^3+3*n|^2*1+3*1|^2*n+1|^3 - (n+1) by SERIES_4: 2
    .= (n|^3 -n) + 3*n|^2 + 3*1|^2*n + 1|^3 -1
    .= 6*i + 3*(n|^2 + 1|^2*n) +1|^3 -1 by z
    .= 6*i + 3*(n|^2 + n) by s
    .= 6*i + 3*(n*n+n) by s2
    .= 6*i + 3*n*(n+1)
    .= 6*i + 6*j by s4
    .= 6*(i+j);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 10

2 divides n*(n-1)
proof
  defpred Q[Nat] means 2 divides $1*($1-1);
  p1: Q[0]
  proof
    0*(0-1)=2*0;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    consider i being Integer such that z: n*(n-1) = 2*i by a1, INT_1:def 9;
    (n+1)*((n+1)-1) = (n+1)*(n+1-1)
    .= 2*(i+n) by z;
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1, p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 11

3 divides 10|^n + 4|^n - 2
proof
  defpred Q[Nat] means 3 divides 10|^$1 + 4|^$1 -2;
  p1: Q[0]
  proof
    w: 10|^0 =1 & 4|^0 =1 by NEWTON:9;
    10|^0 +4|^0 - 2 = 1+1 -2 by w
    .= 2-2 .= 3*0;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    consider i being Integer such that z: 10|^n + 4|^n - 2 = 3*i by a1, INT_1:def 9;
    c: 10|^(n+1) = 10*10|^n &  4|^(n+1) = 4*4|^n by NEWTON:11;
    10|^(n+1) + 4|^(n+1) -2 = 10*10|^n + 4*4|^n -2 by c
    .= 10*(10|^n + 4|^n -2) -6*4|^n +18
    .= 10*3*i - 2*3*4|^n +3*6 by z
    .= 3*(10*i - 2*4|^n +6);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 12

9 divides 10|^n -1
proof
  defpred Q[Nat] means 9 divides 10|^$1 -1;
  p1: Q[0]
  proof
    n: 10|^0 = 1 by NEWTON:9;
    10|^0 - 1 = 0 by n .= 1-1 .= 9*0;
    hence thesis by INT_1: def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    consider i being Integer such that z: 10|^n-1 = 9*i by a1, INT_1:def 9;
    10|^(n+1) -1 = 10*10|^n -1 by NEWTON: 11
    .= 10*(10|^n-1) + 9
    .= 10*9*i + 9 by z
    .= 9*(10*i + 1);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 13

9 divides 4|^n +15*n -1
proof
  defpred Q[Nat] means 9 divides 4|^$1 + 15*$1 -1;
  p1: Q[0]
  proof
    4|^0 = 1 by NEWTON:9;
    then 4|^0 + 15*0 -1 = 0 .= 9*0;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    consider i being Integer such that z: 4|^n + 15*n -1 = 9*i by a1, INT_1:def 9;
    4|^(n+1) + 15*(n+1) -1
    = 4*4|^n + 15*(n+1) -1 by NEWTON: 11
    .= 4*4|^n + 15*n + 14
    .= 4*(4|^n + 15*n - 1) - 3*15*n + 18
    .= 4*9*i - 3*15*n + 18 by z
    .= 9*(4*i - 5*n +2);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 14

6 divides n|^3 + 5*n
proof
  defpred Q[Nat] means 6 divides $1|^3 + 5*$1;
  p1: Q[0]
  proof
    0|^3 = 0 by NEWTON: 16;
    then 0|^3 + 5*0 = 0 .= 6*0;
    hence thesis by INT_1:def 9;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a1: Q[n];
    s1: n|^2 = n|^(1+1) .= n*n|^1 by NEWTON:11 .=n*n by NEWTON:10;
    s2: 2 divides n*(n+1) by Th1;
    consider i being Integer such that z: n|^3 + 5*n = 6*i by a1, INT_1:def 9;
    consider j being Integer such that x: n*(n + 1) = 2*j by s2, INT_1:def 9;
    (n+1)|^3 + 5*(n+1)
    = n|^3 + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5*(n+1) by SERIES_4: 2
    .= n|^3 + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5*n + 5
    .= (n|^3 + 5*n) + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5
    .= 6*i + 3*n|^2*1 + 3*1|^2*n + 1|^3 + 5 by z
    .= 6*i + 3*n|^2 + 3*1|^2*n + 1 + 5 by NEWTON: 15
    .= 6*i + 3*n|^2 + 3*1*n + 1 + 5 by NEWTON: 15
    .= 6*i + 3*n|^2 + 3*n + 6
    .= 6*i + 3*n*n + 3*n + 6 by s1
    .= 6*i + 3*n*(n + 1) + 6
    .= 6*i + 3*2*j +6 by x
    .= 6*(i + j + 1);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
:: 15

theorem
n*n >= n
proof
defpred Q[Nat] means $1*$1>=$1;
p1:Q[0]
proof
0*0>=0;
hence thesis ;
end;
p2:for n st Q[n] holds Q[n+1]
proof
let n;
assume a1: Q[n];
a4:(n+1)*(n+1)=n*n+n+n+1
.= n*n+2*n+1;
a2:n*n+(2*n+1)>=n+(2*n+1) by a1,XREAL_1:8;
a3: 2*n>=0;
(n+1)+(2*n)>=n+1 by a2,a3,a4,XREAL_1:33;
then n*n+2*n+1 >= n+1 by a2,a3, XXREAL_0:2;
hence (n+1)*(n+1)>=n+1 by a4;
end;
for n holds  Q[n] from NAT_1: sch 2(p1,p2);
hence thesis;
end;
theorem
2|^n>=n
proof
defpred Q[Nat] means 2|^$1>=$1;
p1:Q[0]
proof
2|^0>=0;
hence thesis;
end;
p2:for n st Q[n] holds Q[n+1]
proof
let n ;
assume a1:Q[n];
a2: 2|^(n+1) = 2*2|^n by NEWTON:11;
    a3: 2*2|^n >= 2*n by a1, XREAL_1:68;
    per cases;
    suppose s: n=0;
      2|^1 = 2 by NEWTON:10;
      then 2|^(0+1) >= (0+1);
      hence thesis by s;
    end;
    suppose ss: n>0;
      n>=1+0 by ss, INT_1:20;
      then n>=1;
      then n+n >= n+1 by XREAL_1:9;
      then 2|^(n+1) >= n+1 by a2,a3,XXREAL_0:2;
      hence thesis;

end;
end;
for n holds Q[n] from NAT_1: sch 2(p1,p2);
hence thesis ;
end;
::> 212: "environ" expected
::> 213: "begin" missing

::--------------------------------------------------------------------
:: 16

scheme Sch1{P[Nat]}:
    for n holds P[n]
provided
  A1:P[0] and
  A2:P[1] and
  A3:for n st n>=1 & P[n] holds P[n+1]
proof
A4: for n st P[n] holds P[n+1]
proof
   let n such that A5: P[n];
   n=0 or n>=1 by NAT_1: 14;
   hence thesis by A2,A3,A5;
end;
for n holds  P[n]  from NAT_1: sch 2(A1,A4);
hence thesis;
end;

scheme
    NatInd2 { P[Nat] } : for k being non empty Nat holds P[k]
    provided
      E: P[1] and
      D1: for k be non empty Nat st P[k] holds P[k + 1]
  proof
    defpred Q[Nat] means $1 is non empty implies P[$1];
    A: Q[0];
    B: for i be Nat st Q[i] holds Q[i+1]
      proof
        let i be Nat such that C1: Q[i];
        i is non empty implies P[i] by C1;
        per cases;
          suppose i is non empty;
            hence thesis by D1,C1;
          end;
          suppose i is empty;
            hence thesis by E;
          end;
      end;
    for i be Nat holds Q[i] from NAT_1:sch 2 (A,B);
    hence thesis;
  end;

lm1: for n  st n>=1 holds 2*n>=n+1
proof
defpred P[Nat] means 2*$1 >= $1 +1;
A: P[1];
B: for i be non empty  Nat st P[i] holds P[i + 1]
proof
let n be non empty Nat;
assume C1: P[n]; ::czyli 2*n>=n+1;
then 2*n+1 >=n+1 by NAT_1:12;   ::Jezeli a>=b to a+1>=b
then 2*n+1+1>= n+1+1 by XREAL_1:8; :: Jezeli a>=b to a+1>=b+1
hence thesis;
end;
for k being non empty Nat holds P[k] from   NatInd2(A,B);
hence thesis;
end;

2|^n >= n
proof
defpred P[Nat] means 2|^$1>=$1;
A: P[0];
2|^1=2 by  NEWTON: 10;
then B: P[1] ;
C: for n st n>=1 & P[n] holds P[n+1]
proof
let n such that C1: n>=1 & P[n];
2|^n>=n by C1; :: z zalozenia wiemy, ze to zachodzi;
then 2* 2|^n >=2*n by NAT_1:4; ::Jezeli a>=b to c*a>=c*b;
then 2|^(n+1)>= 2*n by NEWTON:11;
then 2|^(n+1)>= 2*n & 2*n>=n+1 by C1,lm1; ::wziete z wczesniej
:: udowodnionego
hence thesis by XXREAL_0:2; ::Jezeli a>=b & b>=c to a>=c
end;
for n holds P[n] from Sch1(A,B,C);
hence thesis;
end;

::--------------------------------------------------------------------
::19

scheme Sch2{P[Nat],m()->Nat}:
    for n st n <= m() holds P[n]
provided
  A1:P[0] and
  A2:for n st n < m() & P[n] holds P[n+1]
proof
  defpred Q[Nat] means $1<=m() implies P[$1];
  A3:Q[0] by A1;
  A4:for n st Q[n] holds Q[n+1]
  proof
    let n such that A5:Q[n];
    assume A6:n+1<=m();
    then n<m() by NAT_1:13;   
    hence thesis by A2,A5;
  end;
  for n holds Q[n] from NAT_1:sch 2(A3,A4);
  hence thesis;
end;

::--------------------------------------------------------------------
::20

scheme Sch3{P[Nat],m()->Nat}:
    for n st n <= m() holds P[n]
provided
  A1:P[m()] and
  A2:for n st n < m() & P[n+1] holds P[n]
proof
  defpred Q[Nat] means $1<=m() implies
    for i st i = m()-$1 holds P[i];
  A3:Q[0] by A1;
  A4:for n st Q[n] holds Q[n+1]
  proof
    let n such that A5:Q[n];
    assume A6:n+1<=m();
    let i such that A7:i=m()-(n+1);
    i< m()-0 & P[i+1] by A6,A5,A7,NAT_1:13,XREAL_1:12;
    hence P[i] by A2,A7;
  end;
  A8:for n holds Q[n] from NAT_1:sch 2(A3,A4);
  let n;
  assume n<=m();
  then reconsider mn=m()-n as Nat by NAT_1:21;

  mn <=m() - 0 & m()-mn=n by XREAL_1:12;
  hence thesis by A8;
end;

::--------------------------------------------------------------------
::21

2 divides n*(n+1)
proof
set n2= n div 2;
n mod 2 < 2 by INT_1: 85;
then A1: n mod 2=0 or n mod 2 = 1 by NAT_1: 23;
per cases by A1;
  suppose n mod 2 = 0;
  then n=2*n2+0 by INT_1: 86;
  then n*(n+1)=2*(n2*(n+1));
  hence thesis by INT_1:def 9;
end;
  suppose n mod 2 = 1;
  then n = 2*n2+1 by INT_1: 86;
  then n*(n+1)=2*((2*n2+1)*(n2+1));
  hence thesis by INT_1:def  9;
end;
end;

::2 Spsoob
2 divides n*(n+1)
proof
defpred P[Nat] means 2 divides $1*($1+1);
0*(0+1)=2*0;
then A1: P[0] by INT_1:def 9;
A2: for n st P[n] holds P[n+1]
proof
let n such that A3: P[n];
consider n2 be Integer such that
A4:n*(n+1)=2*n2 by A3,INT_1:def 9;
(n+1)*(n+2)=n*n+3*n+2
.=n*(n+1)+2*n+2
.=2*n2+2*n+2 by A4
.=2*(n2+n+1);
hence thesis by INT_1:def 9;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;

::--------------------------------------------------------------------
::22

3 divides n*(n+1)*(n+2)
proof
defpred P[Nat] means 3 divides $1*($1+1)*($1+2);
0*(0+1)*(0+2)=0*3;
then A1: P[0] by INT_1:def 9;
A2: for n st P[n] holds P[n+1]
proof
let n such that A3: P[n];
consider k be Integer such that
A4: n*(n+1)*(n+2)= 3*k by A3,INT_1:def 9;
(n+1)*(n+2)*(n+3)=(n*n+3*n+2)*(n+3)
                .=n*(n+1)*(n+2)+3*(n+1)*(n+2)
                .=3*k+3*(n+1)*(n+2) by A4
                .=3*(k+(n+1)*(n+2));
hence thesis by INT_1:def 9;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;

::--------------------------------------------------------------------
::23

lm:3 divides 4|^n+5
proof
defpred P[Nat] means 3 divides 4|^$1+5;
4|^0=1 by NEWTON:9;
then 4|^0+5=3*2;
then A1:P[0] by INT_1:def 9;
A2:for n st P[n] holds P[n+1]
proof
let n such that A3:P[n];
consider k be Integer such that
A4: 4|^n+5 = 3*k by A3,INT_1:def 9;
4|^(n+1)+5=4*4|^n+5 by NEWTON:11
         .=3*k+3*4|^n by A4
         .=3*(k+4|^n);
hence thesis by INT_1:def 9;
end;
for n holds P[n] from NAT_1:sch 2 (A1,A2);
hence thesis;
end;

::--------------------------------------------------------------------
::24

lm: n|^3=n*n*n
proof
n|^(2+1)=n*n|^(1+1) by NEWTON:11
   .=n*(n*n|^1) by NEWTON:11
   .=n*n*n by NEWTON:10;
hence thesis;
end;

lm1:2 divides n*(n+1)
proof
defpred P[Nat] means 2 divides $1*($1+1);
0*(0+1)=2*0;
then A1: P[0] by INT_1:def 9;
A2: for n st P[n] holds P[n+1]
proof
let n such that A3: P[n];
consider n2 be Integer such that
A4:n*(n+1)=2*n2 by A3,INT_1:def 9;
(n+1)*(n+2)=n*n+3*n+2
.=n*(n+1)+2*n+2
.=2*n2+2*n+2 by A4
.=2*(n2+n+1);
hence thesis by INT_1:def 9;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;

::--------------------------------------------------------------------
::25

lm3: (n+1)|^3=(n+1)*(n+1)*(n+1)
proof
(n+1)|^(2+1)=(n+1)*(n+1)|^(1+1) by NEWTON:11
           .=(n+1)*((n+1)*(n+1)|^1) by NEWTON:11
           .=(n+1)*(n+1)*(n+1) by NEWTON:10;
hence thesis;
end;


:: 1^3 + 2^3 + 3^3 + ... + n^3 = n|^2 * (n+1)|^2 / 4
theorem Th6:
  for f st for i holds f.i = i |^ 3
    holds Partial_Sums(f).n = n|^2 * (n+1)|^2 / 4
proof
let f such that A1: for i holds f.i = i|^3;
defpred P[Nat] means Partial_Sums(f).$1 = $1|^2 * ($1+1)|^2 / 4;
A0:0|^2=0 by NEWTON:103;
Partial_Sums(f).0=f.0 by SERIES_1:def 1
                .=0|^3 by A1
                .=0 by NEWTON:103               
                .=0|^2*(0+1)|^2/4 by A0;  ::Tego mi wczeœniej brakowało
then A2: P[0];
A3: for n st P[n] holds P[n+1]
proof
let n such that A5:P[n];
reconsider k=n as Element of NAT by ORDINAL1:def 13;
A7:(n+2)*(n+2)=(n+2)|^2 by lm2;
A6: Partial_Sums(f).(n+1)=Partial_Sums(f).k+f.(n+1) by SERIES_1:def 1
                        .=Partial_Sums(f).k+(n+1)|^3 by A1
                        .=n|^2*(n+1)|^2/4+(n+1)|^3 by A5
                        .=n|^2*(n+1)|^2/4+(n+1)*(n+1)*(n+1) by lm
                        .=n*n*(n+1)|^2/4+(n+1)*(n+1)*(n+1) by lm2
                        .=(n*n)*((n+1)*(n+1))/4+(n+1)*(n+1)*(n+1) by lm2
                        .=((n*n)*(n+1)*(n+1)+4*(n+1)*(n+1)*(n+1))/4
                        .=((n+1)*(n+1))*((n*n)+4*(n+1))/4         ::Teraz chyba
                        .=((n+1)*(n+1))*((n*n)+4*n+4)/4           ::widac skad
                        .=((n+1)*(n+1))*(n+2)|^2/4 by A7          ::wszystko sie
                        .=((n+1)*(n+1))*((n+2)*(n+2))/4 by lm2 ::wzielo by Lecholik
                        .=((n+1)|^2)*((n+2)*(n+2))/4 by lm2
                        .=(n+1)|^2 * (n+2)|^2 / 4 by A7;
hence thesis;
end;
for n holds P[n] from NAT_1:sch 2 (A2,A3);
hence thesis;
end;

::--------------------------------------------------------------------
::26

:: 1 + 3 + 5 + ... + (n-1) = n^2
theorem Th7:
  for f st for i holds f.i = 2*i+1
    holds Partial_Sums(f).n = (n+1)^2
proof
let f such that A1: for i holds f.i=2*i+1;
defpred P[Nat] means Partial_Sums(f).$1=($1+1)^2;
Partial_Sums(f).0=f.0 by SERIES_1:def 1
                .=2*0+1 by A1
                .=1;
then A2: P[0];
A3: for n st P[n] holds P[n+1]
proof
let n such that A5: P[n];
reconsider k=n as Element of NAT by ORDINAL1:def 13;
A6:Partial_Sums(f).(n+1)=Partial_Sums(f).k+f.(n+1) by SERIES_1:def 1
                       .=Partial_Sums(f).k+(2*(n+1)+1) by A1
                       .=(n+1)^2+(2*(n+1)+1) by A5;
                       .=(n+1)*(n+1)+2*n+3
                       .=n*n+2*n+1+2*n+3
                       .=n*n+4*n+4
                       .=(n+2)*(n+2);
hence thesis;
end;
for n holds P[n] from NAT_1:sch 2 (A2,A3);
hence thesis;
end;

::--------------------------------------------------------------------
::27

ex f st f.0=0 & f.1=0 & for n st n>=2 holds f.n=1-1/n
proof
defpred P[set,set] means
   for n st n=$1 holds
    (n=0 implies $2=0) &
    (n=1 implies $2=0) &
    (n>=2 implies $2=1-1/n);
    A1: for x st x in NAT
     ex y st y in REAL & P[x,y]
proof
let x be set;
assume x in NAT;
then reconsider n=x as Element of NAT;
n<2 or n>=2;
then  A2:n=0 or n=1 or n>=2 by NAT_1:27;
per cases by A2;
suppose R:n=0;
take 0;
0 in NAT;
hence thesis by R;
end;
suppose S:n=1;
take 0;
0 in NAT;
hence thesis by S;
end;
suppose T:n>=2;
take 1-1/n;
thus thesis by T,XREAL_0:def 1;
end;
end;
::Te dwie kolejne linijki powinny być troszkę inne, obecne sš wynikiem usilnych prac doprowadzenia zadania do końca, ale brakuje nam jeszcze czegoœ w nagłówku, aby wytłumaczyć dla mizara skšd my to bierzemy, za 2 tygodnie powinniœmy otrzymać odpowiedŸ ;-P
consider f be Real_Sequence such that
A3:for x st x in NAT holds P[x,f.x] from FUNCT_2:sch 1 (A1);
::>                             *103
::hence thesis;
end;
::>,70
:: To treœć kolejnego zadanka którego chyba nikt prócz mnie nie przepisał ;-P Wredny będę i to Wam tu wrzucę, bo ktoœ mnie o to prosił ^^Tak jak wczeœniej brakuje tylko końcówki.
ex f st f.0=0 & f.1=0 & for n st n>=2 holds f.n=1/(n-1)-1/n
proof
defpred P[set,set] means
   for n st n=$1 holds
    (n=0 implies $2=0) &
    (n=1 implies $2=0) &
    (n>=2 implies $2=1/(n-1)-1/n);
    A1: for x st x in NAT
     ex y st y in REAL & P[x,y]
proof
let x be set;
assume x in NAT;
then reconsider n=x as Element of NAT;
n<2 or n>=2;
then  A2:n=0 or n=1 or n>=2 by NAT_1:27;
per cases by A2;
suppose B1:n=0;
take 0;
0 in NAT;
hence thesis by B1;
end;
suppose B2:n=1;
take 0;
0 in NAT;
hence thesis by B2;
end;
suppose B3:n>=2;
take 1/(n-1)-1/n;
thus thesis by B3,XREAL_0:def 1;
end;
end;
hence thesis;
::>        *4
end;

::--------------------------------------------------------------------
::28

lm1: n|^2=n*n
proof
n|^(1+1)=n*n|^1 by NEWTON:11
           .=n*n by NEWTON:10;
hence thesis;
end;

scheme sch1 {n()->Nat,P[Nat]}:
for i st i >= n() holds P[i]
provided
A1: P[n()] and
A2: for i st i >= n() & P[i] holds P[i+1]
proof
  defpred Q[Nat] means P[n()+$1];
B1:Q[0] by A1;
B2: for i st Q[i] holds Q[i+1]
   proof
     let i such that C1:Q[i];
     n()+i>=n()+0 by XREAL_1:8;
     then P[n()+i+1] by C1,A2;
     hence thesis by C1,A2;
   end;
B3:for i holds Q[i] from NAT_1:sch 2(B1,B2);
let i ;
assume i>=n();
then reconsider In = i-n() as Nat by NAT_1:20,21;
Q[In] by B3;
then P[In+n()];
hence thesis;
end;

::--------------------------------------------------------------------
::29

n<>3 &n<>4 implies n|^2<=2|^n
proof
assume A0:n<>3 &n<>4;
now per cases;
   suppose n<4>4;
     then D1:n>=4+1 by NAT_1:13;
     defpred P[Nat] means $1|^2<2>=5 & P[i] holds P[i+1]
        proof
          let i;
          assume F1:i>=5 & P[i];
          then i>=1 by XXREAL_0:2;
          then 2*i+i>=2*i+1 & 5*i>=3*i by XREAL_1:8,66;
          then F2:5*i>=2*i+1 & i*i>=5*i & i*i=i|^2 by XXREAL_0:2,F1,XREAL_1:66,lm1;
          then i|^2>=2*i+1 by XXREAL_0:2;
          then i|^2+i|^2>=i|^2+(2*i+1) & 2*i|^2<2>= i|^2+(2*i+1) by XXREAL_0:2;
          then 2*2|^i >= (i+1)*(i+1) & 2*(2|^i)=2|^(i+1) by F2,NEWTON:11;
          then 2|^(i+1)>=(i+1)|^2 by lm1;
          hence thesis;
        end;
      for i st i>=5 holds P[i] from sch1(B0,B1);
      hence thesis by D1;
     end;
   end;
hence thesis;
end;

::--------------------------------------------------------------------
::30

scheme Sch1{P[Nat]}:
  for n holds P[n]
provided
  A1:P[0] & P[1] & P[2] & P[3] and
  A2:for i st P[3+i] holds P[3+i+1]
proof
  B1:P[0] by A1;
  B2: for n st P[n] holds P[n+1]
    proof
      let n such that C1: P[n];
      per cases by NAT_1:27,28;
         suppose n=0 or n=1 or n=2;
         hence thesis by A1;
         end;
         suppose n >= 3;
         then reconsider n3=n-3 as Element of NAT by NAT_1:21;
         P[n3+3] by C1;
         then P[n3+3+1] by A2;
         hence thesis;
         end;
    end;
for n holds P[n] from NAT_1:sch 2(B1,B2);
hence thesis;
end;

::--------------------------------------------------------------------
::31

scheme Sch2{P[Nat]}:
  for m holds P[m]
provided
  A1:P[0] & P[1] & P[2] and
  A2:for i st P[i] & P[i+1] & P[i+2] holds P[i+3]
proof
  defpred Q[Nat] means for i st i<=$1 holds P[i];
  B1:Q[0] by A1;
  B2:for n st Q[n] holds Q[n+1]
     proof
      let n such that C1: Q[n];
      let i such that C2: i <= n+1;
      per cases by C2,NAT_1:8;
         suppose i<n>=2;
               then reconsider n2=n-2 as Element of NAT by NAT_1:21;
               F1:n2 <= n2 + 2 by NAT_1:19;
               (n2+1)<=(n2+1)+1 by NAT_1:19;
               then P[n2] & P[n2+1] & P[n2+2] by C1,F1;
               then P[n2+3] by A2;
               hence thesis by C3;
             end;
         end;
     end;
for n holds Q[n] from NAT_1:sch 2 (B1,B2);
hence thesis;
end;

::--------------------------------------------------------------------
::32

scheme Sch3 {P[Nat]}:
for n holds P[n]
provided
A1:P[0] and
A2: for n st (for i st i <= n holds P[i]) holds P[n+1]
proof
defpred Q[Nat] means for i st i <= $1 holds P[i];
B1:Q[0] by A1;
B2:for n st Q[n] holds Q[n+1]
  proof
      let n such that C1: Q[n];
      let i such that C2: i <= n+1;
      per cases by C2,NAT_1:8;
       suppose i<=n;
         hence thesis by C1;
       end;
       suppose C3:i=n+1;
         hence thesis by A2,C1;
       end;
  end;
for n holds Q[n] from NAT_1:sch 2(B1,B2);
hence thesis;
end;

::--------------------------------------------------------------------
::33

scheme sch3 {P[Nat]}:
for n holds P[n]
provided
A1: P[0] and
A2: for n st (for i st i<=n holds P[i]) holds P[n+1]
proof
defpred Q[Nat] means for i st i<=$1 holds P[i];
B1: Q[0] by A1;
B2: for n st Q[n] holds Q[n+1]
proof
let n such that Z: Q[n];
let i such that Z1: i<=n+1 ;
per cases by Z1,NAT_1:8;
suppose i<=n;
hence thesis by Z;
end;
suppose C3: i=n+1;
hence thesis by A2,Z;
end;
end;
for n holds Q[n] from NAT_1:sch 2(B1,B2);
hence thesis;
end;

::--------------------------------------------------------------------
::34

n >= 1 implies ex i,j st n = (2|^i) * (2*j+1)
proof
defpred P[Nat] means $1>=1 implies ex i,j st $1=(2|^i) * (2*j+1);
A: P[0];
B: for n st (for i st i<=n holds P[i]) holds P[n+1]
proof
let n such that C0: for i st i<=n holds P[i];
assume C1: n+1>=1;
per cases by NAT_1:14;
suppose n=0;
then Z1: n+1=1;
take i=0,j=0;
(2|^i) * (2*j+1) = (2|^i) * 1
                .= 1*1 by NEWTON:9;
hence thesis by Z1;
end;
suppose n>=1;
consider z being Nat such that Z1: z=2;
set i=n+1 mod 2;
set j=n+1 div 2;
Z0:n+1=j*2+i by INT_1:86;
i<2 by INT_1:85;
then Z1: i=0 or i=1 by NAT_1:23;
per cases by Z1 ;
suppose I: i = 1;
take 0,j;
2|^0=1 by NEWTON:9;
hence thesis by Z0,I;
end;
suppose I: i = 0;
::>   *60
consider z being Nat such that Z5: z=n+1 div 2 by INT_1:def 7;
take 0,j;
(2|^0)*(2*j+1)= 1*(2*j+1) by NEWTON:9
.=1*(2*j+0+1)
.=1*(2*j+i+1) by I
.=1*(n+1+1) by INT_1:86
.=n+2;
end;
end;
end;
for n holds P[n] from sch3(A,B);
hence thesis;
end;

::--------------------------------------------------------------------
::35

<a>|1 = <a>
proof
  A1: len(<a>|1) = 1
   proof
    len<a>=2 by FINSEQ_1:61;
    hence thesis by FINSEQ_1:80;
   end;
  A2: (<a>|1).1=a
   proof
    B1: <a>.1=a by FINSEQ_1:61;
    (<a>|1).1=<a>.1 by FINSEQ_3:121;
    hence thesis by B1;
   end;
  hence thesis by A1,FINSEQ_1:57;
end;

::--------------------------------------------------------------------
::36

t1:<a>=<a>^<b>
proof
A1:len (<a>^<b>)=2
proof
B1:len <a>=1 by FINSEQ_1:57;
B2:len <b>=1 by FINSEQ_1:57;
then len (<a>^<b>)=1+1 by B1,FINSEQ_1:35;
hence thesis;
end;
A2:(<a>^<b>).1=a
proof
thus thesis by FINSEQ_1:58;
end;
A3:(<a>^<b>).2=b
proof
(<a>^<b>).(len <a>+1)=b & len <a>=1
  by FINSEQ_1:57,59;
hence thesis by FINSEQ_1:57;
end;
hence thesis by A1,A2,FINSEQ_1:61;
end;

::--------------------------------------------------------------------
::37

F^<a>^<b>=F^(<a>^<b>)
proof
A5:<a>=<a>^<b> by t1;
A6:len (<a>^<b>)=2
  proof
    B1:len <a>=1 by FINSEQ_1:57;
    B2:len <b>=1 by FINSEQ_1:57;
    then len (<a>^<b>)=1+1 by B1,FINSEQ_1:35;
    hence thesis;
  end;
A7:len (F^(<a>^<b>))= len (F^<a>) by A5;
A8:len (F^<a>)= len F + 2 by A6,A7,FINSEQ_1:35;
A1:len <a>=1 by FINSEQ_1:57;
A2:len (F^<a>) = len F + 1 by A1,FINSEQ_1:35;
A3:len <b>=1 by FINSEQ_1:57;
A4:len (F^<a>^<b>)= len F + 1 + 1 by A2,A3,FINSEQ_1:35;
  then C1:len (F^<a>^<b>)=len (F^(<a>^<b>)) by A8,A7,A5;

for k st  1 <=  k & k <= len (F^<a>^<b>) holds (F^<a>^<b>).k = (F^(<a>^<b>)).k
proof
  let k such that 1 <= k & k <= len (F^<a>^<b>);

end;
::>,70
hence thesis by FINSEQ_1:18,C1;
end;
::> 70: Something remains to be proved

::--------------------------------------------------------------------
::38

theorem Th1:
  for f st for i st 1 <= i & i <= len f holds f.i = i
    holds Sum f = (len f)*(len f+1)/2
proof
defpred P[FinSequence of REAL] means  (for i st 1 <= i & i <= len $1 holds $1.i = i) implies
Sum $1 = (len $1)*(len $1+1)/2;
A: P[<*> REAL]
proof
assume Z1:  for i st 1 <= i & i <= len <*> REAL holds <*>REAL .i = i;
Z2:len <*> REAL=0 by FINSEQ_1:32;
Sum (<*> REAL) = 0 by RVSUM_1:102
.= len (<*> REAL) * (len <*> REAL + 1) /2 by Z2;
hence thesis;
end;
B:  for p being FinSequence of REAL for x being Element of REAL st P[p] holds P[p^<*x*>]
proof
let p being FinSequence of REAL;
let x being Element of REAL;
assume Z2: P[p];
set px=p^<*x*>;
::(for i st 1 <= i & i <= len px holds px.i = i) implies
::Sum px = (len px)*(len px+1)/2
::proof
assume Z3: for i st 1 <= i & i <= len px holds px.i = i;
K1:len px=len p+ len (<*x*>) by FINSEQ_1:35
       .=len p+1 by FINSEQ_1:56;
::K1:len px=len p+1;
K0:1<=len p+1 by NAT_1:11;
K2:x=px.(len px) by K1,FINSEQ_1:59
.= len p+1 by K0,K1,Z3;
for i st 1 <= i & i <= len p holds p.i = i
proof
let i such that Z4: 1<=i & i<= len p;
C1: i<=len p by Z4;
C2: len p<=len p+1 by NAT_1:11;
i <= len p+1 by C1,C2,XXREAL_0:2;
then i <= len px by K1;
then C3:px.i=i by Z3,Z4;
i in dom p by Z4,FINSEQ_3:27;
then px.i=p.i by FINSEQ_1:def 7;
hence thesis by C3;
end;
then K3:Sum p = (len p)*(len p+1)/2 by Z2;
thus Sum px = Sum p+x by RVSUM_1:104
        .= (len px)*(len px+1)/2 by K1,K2,K3;
::end;
end;
for f holds P[f] from FINSEQ_2:sch 2(A,B);
hence thesis;
end;

::--------------------------------------------------------------------
::39

assume z3:for i be Nat st i in Seg len F holds F.i=i;
assume z4: (for i st i in Seg len p holds p.i=i) implies
Sum p = ((len p) * (len p + 1))/2;
assume z5: for i st i in Seg len (p^<x>) holds (p^<x>).i=i;
thus Sum (p^<x>) = ((len (p^<x>)) * (len (p^<x>)+1))/2
proof
Sum (p^<x>)= Sum p + x by RVSUM_1:104
.= (((len p) * (len p + 1))/2) + x by z4,z3,FINSEQ_2:19
::>                                 *4
.= (((len p) * (len p + 1))/2) + (p^<x>).len p +1 by FINSEQ_1:59
.= (((len p) * (len p + 1))/2) + (len p + 1) by z5
::>                                           *4
.= (len p * (len p + 1))/2 + (2 * (len p + 1))/2
.= (len p + 1) * (len p + 2)/2
.= (len p + 1) * (len p + 1 + 1) /2
.= (len (p^<x>)) * (len (p^<x>) +1)/2 by FINSEQ_2:19;
::>                                        *4
hence thesis;
end;
end;
for p  holds Q[p] from FINSEQ_2:sch 2(Z1,Z2);
hence Sum F = ((len F) * (len F+1))/2 by z3;


::--------------------------------------------------------------------
::40

for f being FinSequence of REAL st
for i being Element of NAT st 1 <= i & i <= len f holds f.i = 2*i-1
holds Sum f = (len f)*(len f)
proof
  defpred Q[FinSequence of REAL] means
  (for i being Element of NAT st 1 <= i & i <= len $1 holds $1.i = 2*i-1) implies Sum $1 = (len $1)*(len $1);
  p1: Q[<*>REAL]
  proof
    a: Sum(<*>REAL) = 0 by RVSUM_1:102;
    len (<*>REAL) = 0 by  FINSEQ_1:32;
    then (len (<*>REAL))*(len (<*>REAL)) = 0;
    hence thesis by a;
  end;
  p2: for p,x st Q[p] holds Q[p^<x>]
  proof
    let p,x such that a: Q[p];
::    (for i being Element of NAT st 1<=i & i<= (len p) holds p.i =i) implies (Sum p) = (len p)*(len p + 1)/2 by a;
    thus Q[p^<x>]
    proof
      assume z1: for i being Element of NAT st 1 <= i & i <= len (p^<x>) holds (p^<x>).i = 2*(i)-1;
      z2: len(p^<x>) = len p + 1 by FINSEQ_2:19;
      z3: for i being Element of NAT st 1 <= i & i <= len p holds p.i = 2*i-1
      proof
        let i being Element of NAT such that c: 1 <= i & i<= len p;
        v: i + 0 <= len p + 1 by c, XREAL_1:9;
        len(p^<x>) = len p + 1 by z2;
        then v1: 1 <= i & i <= len(p^<x>) by v, c;
        then v2: (p^<x>).i = 2*i-1 by z1;
        i in dom (p^<x>) & i in dom p by c, v1, FINSEQ_3:27;
        then p.i = (p^<x>).i by FINSEQ_1:def 7 .= 2*i-1 by v2;
        hence thesis;
      end;
      z4: Sum p = (len p)*(len p) by a, z3;
      1 + 0 <= (len p+1) & (len p + 1) <= (len (p^<x>)) by z2, XREAL_1:9;
      then z5: 2*(len (p) + 1) - 1 =(p^<*x*>).(len p + 1) by z1 .= x by FINSEQ_1:59;
      Sum(p^<x>) = Sum p + x by RVSUM_1:104
      .= (len(p))*(len(p)) + x by z4
      .= (len(p))*(len(p)) + (2*len p + 1) by z5
      .= (len(p^<x>))*(len(p^<x>)) by z2;
      hence thesis;
    end;
  end;
  for f being FinSequence of REAL holds Q[f] from FINSEQ_2: sch 2(p1,p2);
  hence thesis;
end;
::> 4: This inference is not accepted

::--------------------------------------------------------------------
::41

scheme Sch1{ P[Nat] } : for n holds P[n]
provided
  a1: P[0] and
  a2: P[1] and
  a3: for n st n>=1 & P[n] holds P[n+1]
proof
  aa: for n st P[n] holds P[n+1]
  proof
    let n such that a: P[n];
    per cases;
    suppose n=0;
      hence thesis by a2;
    end;
    suppose n>0;
      then n >= 0+1 by INT_1:20;
      hence thesis by a,a3;
    end;
  end;
  for n holds P[n] from NAT_1:sch 2(a1,aa);
  hence thesis;
end;

::--------------------------------------------------------------------
::42

theorem
  for f being Real_Sequence st
  for i being Element of NAT holds f.i = 2*i+1 holds
  for n being Element of NAT holds Partial_Sums(f).n = (n+1)*(n+1)
proof
  let f being Real_Sequence such that
  a: for i being Element of NAT holds f.i = 2*i+1;
  defpred Q[Nat] means Partial_Sums(f).$1 = ($1+1)*($1+1);
  p1: Q[0]
  proof
    Partial_Sums(f).0 = f.0 by SERIES_1: def 1
    .= 2*0 + 1 by a
    .= 1;
    hence thesis;
  end;
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that z: Q[n];
    reconsider n1=n as Element of NAT by ORDINAL1:def 13;
    Partial_Sums(f).(n+1) = Partial_Sums(f).n1 + f.(n+1) by SERIES_1:def 1
    .= (n+1)*(n+1) + (2*(n+1)+1) by a,z;
    hence thesis;
  end;

::--------------------------------------------------------------------
::43

theorem
  2 divides (n+1)*(n+2)
proof
  defpred Q[Nat] means 2 divides ($1+1)*($1+2);
  p1: Q[0];
  p2: for n st Q[n] holds Q[n+1]
  proof
    let n such that a: Q[n];
    consider i being Integer such that z: (n+1)*(n+2) = 2*i by a,INT_1:def 9;
    (n+1+1)*(n+2+1)= (n+2)*(n+2+1)
    .= (n+2)*(n+1)+2*(n+2)
    .= 2*i + 2*(n+2) by z
    .= 2*(i+n+2);
    hence thesis by INT_1:def 9;
  end;
  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
::44

for f being FinSequence of REAL st
for i being Element of NAT st 1 <= i & i <= len f holds f.i = i
holds Sum f = (len f)*(len f + 1)/2
proof
  defpred Q[FinSequence of REAL] means
  (for i being Element of NAT st 1 <= i & i <= len $1 holds $1.i = i) implies Sum $1 = (len $1)*(len $1 + 1)/2;
  p1: Q[<*>REAL]
  proof
    a: Sum(<*>REAL) = 0 by RVSUM_1:102;
    len (<*>REAL) = 0 by  FINSEQ_1:32;
    then (len (<*>REAL))*(len (<*>REAL) + 1)/2 = 0;
    hence thesis by a;
  end;
  p2: for p,x st Q[p] holds Q[p^<*x*>]
  proof
    let p,x such that a: Q[p];
::    (for i being Element of NAT st 1<=i & i<= (len p) holds p.i =i) implies (Sum p) = (len p)*(len p + 1)/2 by a;
    thus Q[p^<*x*>]
    proof
      assume z1: for i being Element of NAT st 1 <= i & i <= len (p^<*x*>) holds (p^<*x*>).i = i;
      z2: len(p^<*x*>) = len p + 1 by FINSEQ_2:19;
      z3: for i being Element of NAT st 1 <= i & i <= len p holds p.i = i
      proof
        let i being Element of NAT such that c: 1 <= i & i<= len p;
        v: i + 0 <= len p + 1 by c, XREAL_1:9;
        len(p^<*x*>) = len p + 1 by z2;
        then v1: 1 <= i & i <= len(p^<*x*>) by v, c;
        then v2: (p^<*x*>).i = i by z1;
        i in dom (p^<*x*>) & i in dom p by c, v1, FINSEQ_3:27;
        then p.i = (p^<*x*>).i by FINSEQ_1:def 7 .= i by v2;
        hence thesis;
      end;
      z4: Sum p = (len p)*(len p + 1)/2 by a, z3;
      1 + 0 <= (len p+1) & (len p + 1) <= (len (p^<*x*>)) by z2, XREAL_1:9;
      then z5: len p + 1 = (p^<*x*>).(len p + 1) by z1 .= x by FINSEQ_1:59;
      Sum(p^<*x*>) = Sum p + x by RVSUM_1:104
      .= (len(p)*(len(p) + 1)/2) + x by z4
      .= (len(p)*(len(p) + 1)/2) + (len p + 1) by z5
      .= (len(p^<*x*>))*(len(p^<*x*>) + 1)/2 by z2;
      hence thesis;
    end;
  end;
  for f being FinSequence of REAL holds Q[f] from FINSEQ_2: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
::45

:: 1+2+3+ ... + n = n*(n+1)/2
for f being FinSequence of REAL st
for i being Element of NAT st 1 <= i & i <= len f holds f.i = i
holds Sum f = (len f)*(len f + 1)/2
proof
  defpred Q[FinSequence of REAL] means
  (for i being Element of NAT st 1 <= i & i <= len $1 holds $1.i = i) implies Sum $1 = (len $1)*(len $1 + 1)/2;
  p1: Q[<*>REAL]
  proof
    a: Sum(<*>REAL) = 0 by RVSUM_1:102;
    len (<*>REAL) = 0 by  FINSEQ_1:32;
    hence thesis by a;
  end;
  p2: for p,x st Q[p] holds Q[p^<*x*>]
  proof
    let p,x such that a: Q[p];
    thus Q[p^<*x*>]
    proof
      assume z1: for i being Element of NAT st 1 <= i & i <= len (p^<*x*>) holds (p^<*x*>).i = i;
      z2: len(p^<*x*>) = len p + 1 by FINSEQ_2:19;
      z3: for i being Element of NAT st 1 <= i & i <= len p holds p.i = i
      proof
        let i being Element of NAT such that c: 1 <= i & i<= len p;
        v: i + 0 <= len p + 1 by c, XREAL_1:9;
        len(p^<*x*>) = len p + 1 by z2;
        then v1: 1 <= i & i <= len(p^<*x*>) by v, c;
        then v2: (p^<*x*>).i = i by z1;
        i in dom (p^<*x*>) & i in dom p by c, v1, FINSEQ_3:27;
        then p.i = (p^<*x*>).i by FINSEQ_1:def 7 .= i by v2;
        hence thesis;
      end;
      z4: Sum p = (len p)*(len p + 1)/2 by a, z3;
      1 + 0 <= (len p+1) & (len p + 1) <= (len (p^<*x*>)) by z2, XREAL_1:9;
      then z5: len p + 1 = (p^<*x*>).(len p + 1) by z1 .= x by FINSEQ_1:59;
      Sum(p^<*x*>) = Sum p + x by RVSUM_1:104
      .= (len(p)*(len(p) + 1)/2) + x by z4
      .= (len(p)*(len(p) + 1)/2) + (len p + 1) by z5
      .= (len(p^<*x*>))*(len(p^<*x*>) + 1)/2 by z2;
      hence thesis;
    end;
  end;
  for f being FinSequence of REAL holds Q[f] from FINSEQ_2: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
::46

:: 1^2+2^2+...+n^2 = n*(n+1)*(2*n+1)/6
for f being FinSequence of REAL st
for i being Element of NAT st 1 <= i & i <= len f holds f.i = i|^2
holds Sum f = (len f)*(len f + 1)*(2*(len f) + 1)/6
proof
  defpred Q[FinSequence of REAL] means
  (for i being Element of NAT st 1 <= i & i <= len $1 holds $1.i = i|^2) implies
  (Sum $1 = (len $1)*(len $1 + 1)*(2*(len $1) + 1)/6);
  p1: Q[<*>REAL]
  proof
    a: Sum(<*>REAL) = 0 by RVSUM_1:102;
    len (<*>REAL) = 0 by FINSEQ_1:32;
    hence thesis by a;
  end;
  p2: for p,x st Q[p] holds Q[p^<*x*>]
  proof
    let p,x such that a: Q[p];
    thus Q[p^<*x*>]
    proof
      assume z1: for i being Element of NAT st 1 <= i & i <= len (p^<*x*>) holds (p^<*x*>).i = i|^2;
      z2: len(p^<*x*>) = len p + 1 by FINSEQ_2:19;
      z3: for i being Element of NAT st 1 <= i & i <= len p holds p.i = i|^2
      proof
        let i being Element of NAT such that c: 1 <= i & i<= len p;
        v: i + 0 <= len p + 1 by c, XREAL_1:9;
        len(p^<*x*>) = len p + 1 by z2;
        then v1: 1 <= i & i <= len(p^<*x*>) by v, c;
        then v2: (p^<*x*>).i = i|^2 by z1;
        i in dom (p^<*x*>) & i in dom p by c, v1, FINSEQ_3:27;
        then p.i = (p^<*x*>).i by FINSEQ_1:def 7 .= i|^2 by v2;
        hence thesis;
      end;
      zz: Sum p = (len p)*(len p + 1)*(2*(len p) + 1)/6 by a,z3;
      1 + 0 <= (len p+1) & (len p + 1) <= (len (p^<*x*>)) by z2, XREAL_1:9;
      then z4: (len p + 1)|^2 = (p^<*x*>).(len p + 1) by z1 .= x by FINSEQ_1:59;

      Sum(p^<*x*>) = Sum p + x by RVSUM_1:104
      .= (len p)*(len p + 1)*(2*(len p) + 1)/6 + x by zz
      .= (len p)*(len p + 1)*(2*(len p) + 1)/6 + (len p+1)|^2 by z4
      .= (len p)*(len p + 1)*(2*(len p) + 1)/6 + (len p+1)*(len p+1) by POLYEQ_3:49
      .= (len (p^<*x*>))*(len (p^<*x*>) + 1)*(2*(len (p^<*x*>)) + 1)/6 by z2;
      hence thesis;
    end;
  end;
  for f being FinSequence of REAL holds Q[f] from FINSEQ_2: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
::47

:: 1 + 3 + 5 + ... + (2*n-1) = n*n = n|^2
for f being FinSequence of REAL st
for i being Element of NAT st 1 <= i & i <= len f holds f.i = 2*i-1
holds Sum f = (len f)*(len f)
proof
  defpred Q[FinSequence of REAL] means
  (for i being Element of NAT st 1 <= i & i <= len $1 holds $1.i = 2*i-1) implies Sum $1 = (len $1)*(len $1);
  p1: Q[<*>REAL]
  proof
    a: Sum(<*>REAL) = 0 by RVSUM_1:102;
    len (<*>REAL) = 0 by FINSEQ_1:32;
    hence thesis by a;
  end;
  p2: for p,x st Q[p] holds Q[p^<*x*>]
  proof
    let p,x such that a: Q[p];
    thus Q[p^<*x*>]
    proof
      assume z1: for i being Element of NAT st 1 <= i & i <= len (p^<*x*>) holds (p^<*x*>).i = 2*i-1;
      z2: len(p^<*x*>) = len p + 1 by FINSEQ_2:19;
      z3: for i being Element of NAT st 1 <= i & i <= len p holds p.i = 2*i-1
      proof
        let i being Element of NAT such that c: 1 <= i & i<= len p;
        v: i + 0 <= len p + 1 by c, XREAL_1:9;
        len(p^<*x*>) = len p + 1 by z2;
        then v1: 1 <= i & i <= len(p^<*x*>) by v, c;
        then v2: (p^<*x*>).i = 2*i-1 by z1;
        i in dom (p^<*x*>) & i in dom p by c, v1, FINSEQ_3:27;
        then p.i = (p^<*x*>).i by FINSEQ_1:def 7 .= 2*i-1 by v2;
        hence thesis;
      end;
      zz: Sum p = (len p)*(len p) by a,z3;
      1 + 0 <= (len p+1) & (len p + 1) <= (len (p^<*x*>)) by z2, XREAL_1:9;
      then z4: 2*(len p+1)-1 = (p^<*x*>).(len p + 1) by z1 .= x by FINSEQ_1:59;
      Sum(p^<*x*>) = Sum p + x by RVSUM_1:104
      .= (len p)*(len p) + x by zz
      .= (len p)*(len p) + 2*(len p+1)-1 by z4
      .= (len (p^<*x*>))*(len (p^<*x*>)) by z2;
      hence thesis;
    end;
  end;
  for f being FinSequence of REAL holds Q[f] from FINSEQ_2: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
::48

:: 1^3 + 2^3 + 3^3 + ... + n^3 = n|^2 * (n+1)|^2 / 4
for f being FinSequence of REAL st
for i being Element of NAT st 1 <= i & i <= len f holds f.i = i|^3
holds Sum f = (len f)|^2 * (len f + 1)|^2/4
proof
  defpred Q[FinSequence of REAL] means
  (for i being Element of NAT st 1 <= i & i <= len $1 holds $1.i = i|^3) implies Sum $1 = (len $1)|^2 * (len $1 + 1)|^2/4;
  p1: Q[<*>REAL]
  proof
    a: Sum(<*>REAL) = 0 by RVSUM_1:102;
    b: len (<*>REAL) = 0 by FINSEQ_1:32;
    then len (<*>REAL)|^2 = 0 by NEWTON:16;
    hence thesis by a;
  end;
  p2: for p,x st Q[p] holds Q[p^<*x*>]
  proof
    let p,x such that a: Q[p];
    thus Q[p^<*x*>]
    proof
      assume z1: for i being Element of NAT st 1 <= i & i <= len (p^<*x*>) holds (p^<*x*>).i = i|^3;
      z2: len(p^<*x*>) = len p + 1 by FINSEQ_2:19;
      z3: for i being Element of NAT st 1 <= i & i <= len p holds p.i = i|^3
      proof
        let i being Element of NAT such that c: 1 <= i & i<= len p;
        v: i + 0 <= len p + 1 by c, XREAL_1:9;
        len(p^<*x*>) = len p + 1 by z2;
        then v1: 1 <= i & i <= len(p^<*x*>) by v, c;
        then v2: (p^<*x*>).i = i|^3 by z1;
        i in dom (p^<*x*>) & i in dom p by c, v1, FINSEQ_3:27;
        then p.i = (p^<*x*>).i by FINSEQ_1:def 7 .= i|^3 by v2;
        hence thesis;
      end;
      zz: Sum p = (len p)|^2 * (len p + 1)|^2/4 by a,z3;
      1 + 0 <= (len p+1) & (len p + 1) <= (len (p^<*x*>)) by z2, XREAL_1:9;
      then z4: (len p+1)|^3 = (p^<*x*>).(len p + 1) by z1 .= x by FINSEQ_1:59;
      r: (len p + 1)|^3 = (len p + 1)|^(2+1) .= (len p + 1)*(len p + 1)|^2 by NEWTON: 11;
      Sum(p^<*x*>) = Sum p + x by RVSUM_1:104
      .= (len p)|^2 * (len p + 1)|^2/4 + x by zz
      .= (len p)|^2 * (len p + 1)|^2/4 + (len p + 1)|^3 by z4
      .= (len p)|^2 * (len p + 1)|^2/4 + (len p + 1)*(len p + 1)*(len p + 1) by r, POLYEQ_3:49
      .= (len p)*(len p) * (len p + 1)|^2/4 + (len p + 1)*(len p + 1)*(len p + 1) by POLYEQ_3:49
      .= (len p)*(len p) * ((len p + 1)*(len p + 1))/4 + (len p + 1)*(len p + 1)*(len p + 1) by POLYEQ_3:49
      .= (len (p^<*x*>))*(len (p^<*x*>)) * ((len (p^<*x*>)+1)*(len (p^<*x*>)+1))/4 by z2
      .= (len (p^<*x*>))|^2 * ((len (p^<*x*>)+1)*(len (p^<*x*>)+1))/4 by POLYEQ_3:49
      .= (len (p^<*x*>))|^2 * (len (p^<*x*>) + 1)|^2/4 by POLYEQ_3:49;
      hence thesis;
    end;
  end;
  for f being FinSequence of REAL holds Q[f] from FINSEQ_2: sch 2(p1,p2);
  hence thesis;
end;

  for n holds Q[n] from NAT_1: sch 2(p1,p2);
  hence thesis;
end;

::--------------------------------------------------------------------
::49

for f being FinSequence of REAL st
  for i being Element of NAT st 1 <= i & i <= len f holds f.i = i holds
  Product f = (len f)!
proof
  defpred Q[FinSequence of REAL] means
  (for i being Element of NAT st 1 <= i & i <= len $1 holds $1.i = i) implies Product $1 = (len $1)!;
  p1: Q[<*>REAL]
  proof
    a: Product (<*>REAL) = 1 by RVSUM_1:124;
    (len (<*>REAL))! = (0)! by FINSEQ_1:32 .=1 by NEWTON:18;
    hence thesis by a;
  end;
  p2: for p being FinSequence of REAL, x being Element of REAL st Q[p] holds Q[p^<x>]
  proof
    let p being FinSequence of REAL,x being Element of REAL such that a: Q[p];
    thus Q[p^<x>]
    proof
      assume z1: for i being Element of NAT st 1 <= i & i <= len (p^<x>) holds (p^<x>).i = i;
      z2: len(p^<x>) = len p + 1 by FINSEQ_2:19;
      z3: for i being Element of NAT st 1 <= i & i <= len p holds p.i = i
      proof
        let i being Element of NAT such that c: 1 <= i & i<= len p;
        v: i + 0 <= len p + 1 by c, XREAL_1:9;
        len(p^<x>) = len p + 1 by z2;
        then v1: 1 <= i & i <= len(p^<x>) by v, c;
        then v2: (p^<x>).i = i by z1;
        i in dom (p^<x>) & i in dom p by c, v1, FINSEQ_3:27;
        then p.i = (p^<x>).i by FINSEQ_1:def 7 .= i by v2;
        hence thesis;
      end;
      z4: Product p = (len p)! by a,z3;
      d: 0 <= len p by NAT_1:2;
      1 + 0 <= (len p+1) & (len p + 1) <= (len (p^<x>)) by z2,d, XREAL_1:9;
      then z5: len p + 1 = (p^<x>).(len p + 1) by z1 .= x by FINSEQ_1:59;
      Product (p^<x>) = Product p * x by RVSUM_1:126
      .= (len p)! * x by z4
      .= (len p)! * (len p + 1) by z5
      .= (len (p^<x>))! by NEWTON: 21,z2;
      hence thesis;
    end;
  end;
  for f being FinSequence of REAL holds Q[f] from FINSEQ_2: sch 2(p1,p2);
  hence thesis;
end;