:: Recursive Definitions
:: by Krzysztof Hryniewiecki
::
:: Received September 4, 1989
:: Copyright (c) 1990-2026 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, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, FUNCT_1,
RELAT_1, TARSKI, VALUED_0, CARD_1, ARYTM_3, ORDINAL1, CLASSES1, ZFMISC_1,
ORDINAL2, FUNCOP_1, MCART_1, NAT_1, ORDINAL4, ARYTM_1, REAL_1, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, SUBSET_1, ORDINAL1,
XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1,
ORDINAL2, NUMBERS, CLASSES1, FINSEQ_1, FUNCT_2, BINOP_1, DOMAIN_1,
VALUED_0;
constructors BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, FINSEQ_1,
VALUED_0, CLASSES1, ORDINAL2, RELSET_1, XTUPLE_0, XREAL_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, RELSET_1,
FINSEQ_1, VALUED_0, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_1, RELAT_1;
equalities BINOP_1;
expansions TARSKI, FUNCT_1, RELAT_1;
theorems TARSKI, NAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, RELAT_1, XBOOLE_1,
FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, CLASSES1, ORDINAL2, XBOOLE_0,
ZFMISC_1, PARTFUN1, XREAL_0, NUMBERS;
schemes NAT_1, FINSEQ_1, BINOP_1, CLASSES1, ORDINAL1, FUNCT_2;
begin
reserve n,m,k for Nat,
D for non empty set,
Z,x,y,z,y1,y2 for set,
p,q for FinSequence;
Lm1: for p being FinSequence of D st 1 <= n & n <= len p holds p.n is Element
of D
proof
let p be FinSequence of D;
assume 1 <= n & n <= len p;
then n in Seg len p by FINSEQ_1:1;
then n in dom p by FINSEQ_1:def 3;
then
A1: p.n in rng p by FUNCT_1:def 3;
rng p c= D by FINSEQ_1:def 4;
hence thesis by A1;
end;
definition
let p be natural-valued Function;
let n be set;
redefine func p.n -> Element of NAT; :: redefines . (FUNCT_1, definition)
coherence by ORDINAL1:def 12;
end;
:: Schemes of existence
scheme
RecEx{A() -> object,P[object,object,object]}:
ex f being Function st dom f = NAT & f.0 =
A() & for n being Nat holds P[n,f.n,f.(n+1)]
provided
A1: for n being Nat for x being set ex y being set st P[n,x,y ];
defpred Q[set,set,set] means ex O2 being Ordinal st O2 = $3 & (for X being
set, n being Nat st X c= Rank the_rank_of $2 ex Y being set st Y c=
Rank O2 & P[n,X,Y]) &
(for O being Ordinal st for X being set, n being Nat
st X c= Rank the_rank_of $2 ex Y being set st Y c= Rank O & P[n,X,Y]
holds O2 c= O);
A2: for n being Nat for x being set ex y being set st Q[n,x,y]
proof
defpred Y[object,object] means for m being Nat ex y being set st $2
is Ordinal & y c= Rank the_rank_of $2 & P[m,$1,y];
let n be Nat;
let x be set;
defpred X[Ordinal] means for X being set, n being Nat st X c=
Rank the_rank_of x ex Y being set st Y c= Rank $1 & P[n,X,Y];
A3: for x9 being object st x9 in bool Rank the_rank_of x
ex o being object st Y[x9,o]
proof
let x9 be object;
assume x9 in bool Rank the_rank_of x;
defpred X[object,object] means
ex y being set st $2 is Ordinal & y c= Rank
the_rank_of $2 & P[$1,x9,y];
A4: for e being object st e in NAT ex u being object st X[e,u]
proof
let i be object;
assume i in NAT;
then reconsider i9 = i as Nat;
thus ex o being object, y being set st o is Ordinal & y c= Rank
the_rank_of o & P[i,x9,y]
proof
x9 is set by TARSKI:1;
then consider y being set such that
A5: P[i9,x9,y] by A1;
take o = the_rank_of y, y;
thus o is Ordinal;
the_rank_of the_rank_of y = the_rank_of y by CLASSES1:73;
hence y c= Rank the_rank_of o by CLASSES1:65;
thus thesis by A5;
end;
end;
consider h being Function such that
A6: dom h = NAT and
A7: for i being object st i in NAT holds X[i,h.i] from CLASSES1:sch 1(
A4);
take o = sup rng h;
thus for m being Nat ex y being set st o is Ordinal & y c=
Rank the_rank_of o & P[m,x9,y]
proof
let m be Nat;
A8: m in NAT by ORDINAL1:def 12;
then consider y being set such that
A9: h.m is Ordinal and
A10: y c= Rank the_rank_of (h.m) and
A11: P[m,x9,y] by A7;
reconsider O = h.m as Ordinal by A9;
h.m in rng h by A6,A8,FUNCT_1:def 3;
then h.m in sup rng h by A9,ORDINAL2:19;
then h.m c= o by ORDINAL1:def 2;
then
A12: Rank O c= Rank o by CLASSES1:37;
take y;
thus o is Ordinal;
y c= Rank O by A10,CLASSES1:73;
then y c= Rank o by A12;
hence y c= Rank the_rank_of o by CLASSES1:73;
thus thesis by A11;
end;
end;
consider f being Function such that
A13: dom f = bool Rank the_rank_of x and
A14: for x9 being object st x9 in bool Rank the_rank_of x holds Y[x9,f.x9
] from CLASSES1:sch 1(A3);
A15: ex O being Ordinal st X[O]
proof
take O2 = sup rng f;
thus for X being set, m being Nat st X c= Rank the_rank_of x
ex Y being set st Y c= Rank O2 & P[m,X,Y]
proof
let X be set;
let m be Nat;
assume
A16: X c= Rank the_rank_of x;
then consider Y being set such that
A17: f.X is Ordinal and
A18: Y c= Rank the_rank_of (f.X) and
A19: P[m,X,Y] by A14;
reconsider O = f.X as Ordinal by A17;
f.X in rng f by A13,A16,FUNCT_1:def 3;
then f.X in sup rng f by A17,ORDINAL2:19;
then f.X c= O2 by ORDINAL1:def 2;
then
A20: Rank O c= Rank O2 by CLASSES1:37;
take Y;
the_rank_of O = O by CLASSES1:73;
hence Y c= Rank O2 by A18,A20;
thus thesis by A19;
end;
end;
consider O2 being Ordinal such that
A21: X[O2] & for O being Ordinal st X[O] holds O2 c= O from ORDINAL1:
sch 1(A15);
take O2;
thus thesis by A21;
end;
A22: for n being Nat for x,y1,y2 being set st Q[n,x,y1] & Q[n,x,
y2] holds y1 = y2
proof
let n be Nat;
let x,y1,y2 be set;
assume that
A23: Q[n,x,y1] and
A24: Q[n,x,y2];
consider O2 being Ordinal such that
A25: O2 = y2 and
A26: ( for X being set, n being Nat st X c= Rank
the_rank_of x ex Y being set st Y c= Rank O2 & P[n,X,Y])& for O being Ordinal
st for X being set, n being Nat st X c= Rank the_rank_of x ex Y
being set st Y c= Rank O & P[n,X,Y] holds O2 c= O by A24;
consider O1 being Ordinal such that
A27: O1 = y1 and
A28: ( for X being set, n being Nat st X c= Rank
the_rank_of x ex Y being set st Y c= Rank O1 & P[n,X,Y])& for O being Ordinal
st for X being set, n being Nat st X c= Rank the_rank_of x ex Y
being set st Y c= Rank O & P[n,X,Y] holds O1 c= O by A23;
O1 c= O2 & O2 c= O1 by A28,A26;
hence thesis by A27,A25,XBOOLE_0:def 10;
end;
ex f being Function st dom f = NAT & f.0 = the_rank_of A() & for n
being Nat holds Q[n,f.n,f.(n+1)]
proof
deffunc S(Nat) = {k : k <= $1};
A29: for p,q being Function,k st dom p = S(k) & dom q = S(k+1) & p.0 = q.0
& for n st n < k holds Q[n,p.n,p.(n+1)] & Q[n,q.n,q.(n+1)] holds p.k = q.k
proof
let p,q be Function;
let k;
defpred Z[Nat] means $1 <= k implies p.$1 = q.$1;
assume that
dom p = S(k) and
dom q = S(k+1) and
A30: p.0 = q.0 and
A31: for n st n < k holds Q[n,p.n,p.(n+1)] & Q[n,q.n,q.(n+1)];
A32: for n st Z[n] holds Z[n+1]
proof
let n;
assume
A33: n <= k implies p.n = q.n;
assume n+1 <= k;
then
A34: n < k by NAT_1:13;
then
A35: Q[n,p.n,p.(n+1)] by A31;
Q[n,p.n,q.(n+1)] by A31,A33,A34;
hence thesis by A22,A35;
end;
A36: Z[0] by A30;
for n holds Z[n] from NAT_1:sch 2(A36,A32);
hence thesis;
end;
A37: for n ex p being Function st dom p = S(n) & p.0 = the_rank_of A() &
for k st k < n holds Q[k,p.k,p.(k+1)]
proof
defpred Z[Nat] means
ex p being Function st dom p = S($1) & p
.0 = the_rank_of A() & for k st k < $1 holds Q[k,p.k,p.(k+1)];
A38: for n st Z[n] holds Z[n+1]
proof
let n;
given p being Function such that
dom p = S(n) and
A39: p.0 = the_rank_of A() and
A40: for k st k < n holds Q[k,p.k,p.(k+1)];
consider z such that
A41: Q[n,p.n,z] by A2;
defpred ST[object,object] means
(for k st k=$1 holds (k <= n implies $2 = p.
k) & (k=n+1 implies $2 = z ));
A42: for x being object st x in S(n+1) ex y being object st ST[x,y]
proof
let x be object;
assume x in S(n+1);
then
A43: ex m st m=x & m <= n+1;
then reconsider t=x as Nat;
A44: t <= n implies thesis
proof
assume
A45: t <= n;
take p.x;
let k;
assume
A46: k=x;
hence k <= n implies p.x = p.k;
assume k=n+1;
then n+1 <= n+0 by A45,A46;
hence thesis by XREAL_1:6;
end;
t = n+1 implies thesis
proof
assume
A47: t=n+1;
take z;
let k such that
A48: k=x;
thus k <= n implies z=p.k
proof
assume k <= n;
then n+1 <= n+0 by A47,A48;
hence thesis by XREAL_1:6;
end;
thus thesis;
end;
hence thesis by A43,A44,NAT_1:8;
end;
consider q being Function such that
A49: dom q = S(n+1) &
for x being object st x in S(n+1) holds ST[x,q.x] from
CLASSES1:sch 1 (A42);
take q;
thus dom q = S(n+1) by A49;
0 in S(n+1);
hence q.0 = the_rank_of A() by A39,A49;
let k such that
A50: k < n+1;
A51: now
A52: k+1 <= n+1 by A50,NAT_1:13;
assume k <> n;
then k+1 <> n+1;
then
A53: k+1 <= n by A52,NAT_1:8;
then
A54: k < n by NAT_1:13;
k+1 in S(n+1) by A52;
then
A55: q.(k+1) = p.(k+1) by A49,A53;
k in S(n+1) by A50;
then p.k = q.k by A49,A54;
hence thesis by A40,A55,A54;
end;
now
assume
A56: k = n;
then k <= n+1 by NAT_1:11;
then k in S(n+1);
then
A57: q.k = p.k by A49,A56;
k+1 in S(n+1) by A56;
then q.(k+1) = z by A49,A56;
hence thesis by A41,A56,A57;
end;
hence thesis by A51;
end;
A58: Z[0]
proof
set s = S(0) --> the_rank_of A();
take s;
thus dom s = S(0) by FUNCOP_1:13;
0 in S(0);
hence s.0 = the_rank_of A() by FUNCOP_1:7;
thus thesis;
end;
thus for n holds Z[n] from NAT_1:sch 2(A58,A38);
end;
ex f being Function st dom f = NAT & for n ex p being Function st dom
p = S(n) & p.0 = the_rank_of A() & (for k st k < n holds Q[k,p.k,p.(k+1)]) & f.
n = p.n
proof
defpred Z[object,object] means
for n st n=$1 ex p being Function st dom p = S(
n) & p.0 = the_rank_of A() & (for k st k < n holds Q[k,p.k,p.(k+1)]) & $2 = p.n
;
A59: for x being object st x in NAT ex y being object st Z[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n=x as Nat;
consider p being Function such that
A60: dom p = S(n) & p.0 = the_rank_of A() & for k st k < n holds Q
[k,p.k,p.(k +1)] by A37;
take p.n;
let k such that
A61: k = x;
take p;
thus thesis by A60,A61;
end;
consider f being Function such that
A62: dom f = NAT &
for x being object st x in NAT holds Z[x,f.x] from CLASSES1:
sch 1 (A59);
take f;
thus dom f = NAT by A62;
let n;
n in NAT by ORDINAL1:def 12;
then consider p being Function such that
A63: dom p = S(n) & p.0 = the_rank_of A() and
A64: for k st k < n holds Q[k,p.k,p.(k+1)] and
A65: f.n = p.n by A62;
take p;
thus dom p = S(n) & p.0 = the_rank_of A() by A63;
thus for k st k < n holds Q[k,p.k,p.(k+1)] by A64;
thus thesis by A65;
end;
then consider f being Function such that
A66: dom f = NAT and
A67: for n ex p being Function st dom p = S(n) & p.0 = the_rank_of A(
) & (for k st k < n holds Q[k,p.k,p.(k+1)]) & f.n = p.n;
take f;
thus dom f = NAT by A66;
ex p being Function st dom p = S(0) & p.0 = the_rank_of A() & (for k
st k < 0 holds Q[k,p.k,p.(k+1)]) & f.0 = p.0 by A67;
hence f.0 = the_rank_of A();
let d be Nat;
consider p being Function such that
A68: dom p = S(d+1) and
A69: p.0 = the_rank_of A() and
A70: for k st k < d+1 holds Q[k,p.k,p.(k+1)] and
A71: f.(d+1) = p.(d+1) by A67;
consider q being Function such that
A72: dom q = S(d) and
A73: q.0 = the_rank_of A() and
A74: for k st k < d holds Q[k,q.k,q.(k+1)] and
A75: f.d = q.d by A67;
dom p = S(d+1) & dom q = S(d) & p.0 = q.0 & for k st k < d holds Q[k
,q.k,q.(k+1)] & Q[k,p.k,p.(k+1)]
proof
thus dom p = S(d+1) by A68;
thus dom q = S(d) by A72;
thus p.0 = q.0 by A69,A73;
let k;
assume
A76: k < d;
hence Q[k,q.k,q.(k+1)] by A74;
d <= d+1 by NAT_1:11;
then k < d+1 by A76,XXREAL_0:2;
hence thesis by A70;
end;
then p.d = q.d by A29;
hence thesis by A70,A71,A75,XREAL_1:29;
end;
then consider g being Function such that
A77: dom g = NAT and
A78: g.0 = the_rank_of A() and
A79: for n being Nat holds Q[n,g.n,g.(n+1)];
defpred X[object,object] means
ex i being Nat st i = $1`2 & P[$1`2,$1`1
,$2`1] & $2`2 = i+1 & not ex y being set st P[$1`2,$1`1,y] & the_rank_of y in
the_rank_of $2`1;
A80: [A(),0]`1 = A() & [A(),0]`2 = 0;
set beta = sup rng g;
A81: for x being object st x in [:Rank beta, NAT:]
ex u being object st X[x,u]
proof
let x be object;
defpred X[Ordinal] means ex y being set st y c= Rank $1 & P[x`2,x`1,y];
assume x in [:Rank beta, NAT:];
then consider a,b being object such that
A82: a in Rank beta and
A83: b in NAT and
A84: x = [a,b] by ZFMISC_1:def 2;
reconsider b as Nat by A83;
A85: x`2 = b & x`1 = a by A84;
the_rank_of a in beta by A82,CLASSES1:66;
then consider alfa being Ordinal such that
A86: alfa in rng g and
A87: the_rank_of a c= alfa by ORDINAL2:21;
consider k being object such that
A88: k in dom g and
A89: alfa = g.k by A86,FUNCT_1:def 3;
reconsider k as Nat by A77,A88;
A90: Q[k,alfa,g.(k+1)] by A79,A89;
then reconsider O2 = g.(k+1) as Ordinal;
reconsider a as set by TARSKI:1;
a c= Rank alfa by A87,CLASSES1:65;
then a c= Rank the_rank_of alfa by CLASSES1:73;
then ex y being set st y c= Rank O2 & P[x`2,x`1,y] by A90,A85;
then
A91: ex O being Ordinal st X[O];
consider O being Ordinal such that
A92: X[O] and
A93: for O9 being Ordinal st X[O9] holds O c= O9 from ORDINAL1:sch 1(
A91);
consider Y being set such that
A94: Y c= Rank O and
A95: P[b,a,Y] by A85,A92;
A96: the_rank_of Y c= O by A94,CLASSES1:65;
take u = [Y,b+1], i = b;
thus i = x`2 by A84;
thus P[x`2,x`1,u`1] by A85,A95;
thus u`2 = i+1;
given y being set such that
A97: P[x`2,x`1,y] and
A98: the_rank_of y in the_rank_of u`1;
A99: y c= Rank the_rank_of y by CLASSES1:def 9;
the_rank_of y in the_rank_of Y by A98;
hence contradiction by A93,A97,A96,A99,ORDINAL1:5;
end;
consider F being Function such that
dom F = [:Rank beta, NAT:] and
A100: for x being object st x in [:Rank beta, NAT:] holds X[x,F.x] from
CLASSES1:sch 1(A81);
deffunc U(Nat,set) = (F.[$2,$1])`1;
consider f being Function such that
A101: dom f = NAT and
A102: f.0 = A() and
A103: for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1:sch 11;
defpred X[Nat] means the_rank_of (f.$1) in sup rng g;
g.0 in rng g by A77,FUNCT_1:def 3;
then
A104: X[0] by A78,A102,ORDINAL2:19;
A105: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat;
assume
A106: the_rank_of (f.n) in sup rng g;
then consider o1 being Ordinal such that
A107: o1 in rng g and
A108: the_rank_of (f.n) c= o1 by ORDINAL2:21;
A109: n in NAT by ORDINAL1:def 12;
f.n in Rank sup rng g by A106,CLASSES1:66;
then
A110: [f.n,n] in [:Rank beta, NAT:] by A109,ZFMISC_1:87;
consider m being object such that
A111: m in dom g and
A112: g.m = o1 by A107,FUNCT_1:def 3;
reconsider m as Nat by A77,A111;
consider o2 being Ordinal such that
A113: o2 = g.(m+1) and
A114: for X being set, n being Nat st X c= Rank the_rank_of
(g.m) ex Y being set st Y c= Rank o2 & P[n,X,Y] and
for o being Ordinal st for X being set, n being Nat st X c=
Rank the_rank_of (g.m) ex Y being set st Y c= Rank o & P[n,X,Y] holds o2 c= o
by A79;
the_rank_of (f.n) c= the_rank_of (g.m) by A108,A112,CLASSES1:73;
then f.n c= Rank the_rank_of (g.m) by CLASSES1:65;
then consider YY being set such that
A115: YY c= Rank o2 and
A116: P[n,f.n,YY] by A114;
A117: the_rank_of YY c= o2 by A115,CLASSES1:65;
[f.n,n]`1 = f.n & [f.n,n]`2 = n;
then ex i being Nat st i = n &( P[n,f.n,(F.[f.n,n]) `1])& (F.[f
.n,n])`2 = i+1 & not ex y being set st P[n,f.n,y] & the_rank_of y in
the_rank_of (F.[f.n,n])`1 by A100,A110;
then
A118: the_rank_of (F.[f.n,n])`1 c= the_rank_of YY by A116,ORDINAL1:16;
g.(m+1) in rng g by A77,FUNCT_1:def 3;
then
A119: o2 in sup rng g by A113,ORDINAL2:19;
f.(n+1) = (F.[f.n,n])`1 by A103;
hence thesis by A118,A117,A119,ORDINAL1:12,XBOOLE_1:1;
end;
A120: for n being Nat holds X[n] from NAT_1:sch 2(A104,A105);
defpred X[Nat] means P[$1,f.$1,f.($1+1)];
A121: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat;
assume P[n,f.n,f.(n+1)];
the_rank_of (f.(n+1)) in sup rng g by A120;
then f.(n+1) in Rank sup rng g by CLASSES1:66;
then
A122: [f.(n+1),n+1] in [:Rank beta, NAT:] by ZFMISC_1:87;
[f.(n+1),n+1]`1 = f.(n+1) & [f.(n+1),n+1]`2 = n+1;
then ex i being Nat st i = n+1 &( P[n+1,f.(n+1),(F.[ f.(n+1),n+
1])`1])& (F.[f.(n+1),n+1])`2 = i+1 & not ex y being set st P[(n+1), f.(n+1),y]
& the_rank_of y in the_rank_of (F.[f.(n+1),n+1])`1 by A100,A122;
hence thesis by A103;
end;
take f;
thus dom f = NAT by A101;
thus f.0 = A() by A102;
A() in Rank sup rng g by A102,A104,CLASSES1:66;
then [A(),0] in [:Rank beta, NAT:] by ZFMISC_1:87;
then ex i being Nat st i = [A(),0]`2 &( P[0,A(),(F.[ A(),0])`1])&
(F.[A(),0])`2 = i+1 & not ex y being set st P[0,A(),y] & the_rank_of y in
the_rank_of (F.[A(),0])`1 by A100,A80;
then
A123: X[0] by A102,A103;
thus for n being Nat holds X[n] from NAT_1:sch 2(A123,A121);
end;
scheme
RecExD{D()->non empty set,A() -> Element of D(), P[object,object,object]}:
ex f being sequence of D() st f.0 = A() &
for n being Nat holds P[n,f.n,f.(n+1)]
provided
A1: for n being Nat for x being Element of D() ex y being
Element of D() st P[n,x,y]
proof
defpred Q[Nat,set,set] means P[$1,$2,$3];
A2: for x being Element of NAT for y being Element of D()
ex z being Element of D() st Q[x,y,z] by A1;
consider f being Function of [:NAT,D():],D() such that
A3: for x being Element of NAT for y being Element of
D() holds Q[x,y,f.(x,y)] from BINOP_1:sch 3(A2);
defpred P[FinSequence] means ($1.1=A() & for n st n+2 <= len $1 holds $1.(n+
2) = f.[n,$1.(n+1)]);
consider X being set such that
A4: for x being object holds x in X iff
ex p st p in D()* & P[p] & x=p from FINSEQ_1:
sch 4;
set Y = union X;
A5: x in X implies x in D()*
proof
assume x in X;
then
ex p st p in D()* & (p.1=A() & for n st n + 2 <= len p holds p.(n+2) =
f.[n,p.(n+1)]) & x=p by A4;
hence thesis;
end;
A6: for p,q st p in X & q in X & len p <= len q holds p c= q
proof
let p,q;
assume that
A7: p in X and
A8: q in X and
A9: len p <= len q;
A10: ex q9 being FinSequence st q9 in D()* & (q9.1 = A() & for n st n+2<=
len q9 holds q9.(n+2) = f.[n,q9.(n+1)]) & q=q9 by A4,A8;
A11: ex p9 being FinSequence st p9 in D()* & (p9.1 = A() & for n st n+2<=
len p9 holds p9.(n+2) = f.[n,p9.(n+1)]) & p=p9 by A4,A7;
A12: for n st 1 <= n & n <= len p holds p.n = q.n
proof
defpred P[Nat] means 1 <= $1 & $1 <= len p & p.$1 <> q.$1;
assume ex n st P[n];
then
A13: ex n be Nat st P[n];
consider k be Nat such that
A14: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5(A13);
k = 1
proof
0 <> k by A14;
then consider n being Nat such that
A15: k = n+1 by NAT_1:6;
n+0 <= n+1 by XREAL_1:7;
then
A16: n <= len p by A14,A15,XXREAL_0:2;
A17: n+0 < n+1 by XREAL_1:6;
assume
A18: k <> 1;
then 1 < n+1 by A14,A15,XXREAL_0:1;
then
A19: 1 <= n by NAT_1:13;
n <> 0 by A18,A15;
then consider m being Nat such that
A20: n=m+1 by NAT_1:6;
reconsider m as Nat;
A21: m+2 <= len q by A9,A14,A15,A20,XXREAL_0:2;
p.k = p.(m+(1+1)) by A15,A20
.=f.[m,p.n] by A11,A14,A15,A20
.=f.[m,q.(m+1)] by A14,A15,A19,A16,A17,A20
.=q.k by A10,A15,A20,A21;
hence thesis by A14;
end;
hence contradiction by A11,A10,A14;
end;
now
let x be object;
assume x in p;
then consider n be Nat such that
A22: n in dom p and
A23: x = [n,p.n] by FINSEQ_1:12;
A24: n in Seg len p by A22,FINSEQ_1:def 3;
then
A25: 1 <= n by FINSEQ_1:1;
A26: n <= len p by A24,FINSEQ_1:1;
then n <= len q by A9,XXREAL_0:2;
then n in Seg len q by A25,FINSEQ_1:1;
then
A27: n in dom q by FINSEQ_1:def 3;
x = [n,q.n] by A12,A23,A25,A26;
hence x in q by A27,FUNCT_1:1;
end;
hence thesis;
end;
A28: Y is Function-like
proof
let x,y,z being object such that
A29: [x,y] in Y and
A30: [x,z] in Y;
consider Z2 being set such that
A31: [x,z] in Z2 and
A32: Z2 in X by A30,TARSKI:def 4;
Z2 in D()* by A5,A32;
then reconsider q=Z2 as FinSequence of D() by FINSEQ_1:def 11;
consider Z1 being set such that
A33: [x,y] in Z1 and
A34: Z1 in X by A29,TARSKI:def 4;
Z1 in D()* by A5,A34;
then reconsider p=Z1 as FinSequence of D() by FINSEQ_1:def 11;
per cases;
suppose len q <= len p;
then
A35: q c= Z1 by A6,A34,A32;
[x,y] in p by A33;
hence thesis by A31,A35,FUNCT_1:def 1;
end;
suppose len p <= len q;
then p c= Z2 by A6,A34,A32;
then [x,y] in q by A33;
hence thesis by A31,FUNCT_1:def 1;
end;
end;
Y is Relation-like
proof let x be object;
assume x in Y;
then consider Z2 being set such that
A36: x in Z2 and
A37: Z2 in X by TARSKI:def 4;
ex p st p in D()* & P[p] & Z2=p by A4,A37;
then Z2 is Relation-like;
hence ex y,z being object st x = [y,z] by A36;
end;
then consider g being Function such that
A38: g = Y by A28;
A39: for x being object st x in rng g holds x in D()
proof
let x be object;
assume x in rng g;
then consider y being object such that
A40: y in dom g & x = g.y by FUNCT_1:def 3;
[y,x] in Y by A38,A40,FUNCT_1:1;
then consider Z such that
A41: [y,x] in Z and
A42: Z in X by TARSKI:def 4;
Z in D()* by A5,A42;
then reconsider p=Z as FinSequence of D() by FINSEQ_1:def 11;
y in dom p & x = p.y by A41,FUNCT_1:1;
then
A43: x in rng p by FUNCT_1:def 3;
rng p c= D() by FINSEQ_1:def 4;
hence thesis by A43;
end;
then rng g c= D();
then reconsider h = g as Function of dom g,D() by FUNCT_2:2;
A44: for n holds (n+1) in dom h
proof
defpred P[Nat] means $1+1 in dom h;
A45: for n st n+2 <= len <*A()*> holds <*A()*>.(n+2) = f.[n,<*A()*>.(n+1)]
proof
let n;
assume n+2 <= len <*A()*>;
then n+2 <= 1 by FINSEQ_1:39;
then n+(1+1) <= n+1 by NAT_1:12;
hence thesis by XREAL_1:6;
end;
<*A()*>.1 = A() & <*A()*> in D()* by FINSEQ_1:def 11;
then <*A()*> in X by A4,A45;
then
A46: {[1,A()]} in X by FINSEQ_1:37;
A47: for k st P[k] holds P[k+1]
proof
let k;
assume k+1 in dom h;
then [k+1,h.(k+1)] in Y by A38,FUNCT_1:1;
then consider Z such that
A48: [k+1,h.(k+1)] in Z and
A49: Z in X by TARSKI:def 4;
Z in D()* by A5,A49;
then reconsider Z as FinSequence of D() by FINSEQ_1:def 11;
A50: k+1 = len Z implies thesis
proof
set p=Z^<*f.[k,Z.(k+1)]*>;
A51: 1 <= k+1+1 by NAT_1:12;
assume
A52: k+1 = len Z;
then 1 <= len Z by NAT_1:12;
then 1 in Seg len Z by FINSEQ_1:1;
then
A53: 1 in dom Z by FINSEQ_1:def 3;
A54: for n st n+2 <= len p holds p.(n+2) = f.[n,p.(n+1)]
proof
let n;
assume n+2 <= len p;
then
A55: n+2 <= len Z + len <*f.[k,Z.(k+1)]*> by FINSEQ_1:22;
then
A56: n+2 <= len Z + 1 by FINSEQ_1:40;
A57: n+2 <> len Z + 1 implies thesis
proof
n+1+1 <= len Z + 1 by A55,FINSEQ_1:40;
then 1 <= n + 1 & n+1 <= len Z by NAT_1:12,XREAL_1:6;
then n+1 in Seg len Z by FINSEQ_1:1;
then
A58: n+1 in dom Z by FINSEQ_1:def 3;
A59: 1 <= n+(1+1) by NAT_1:12;
assume
A60: n+2 <> len Z + 1;
then n+2 <= len Z by A56,NAT_1:8;
then n+2 in Seg len Z by A59,FINSEQ_1:1;
then
A61: n+2 in dom Z by FINSEQ_1:def 3;
ex q st q in D()* & q.1 = A() & (for n st n+2 <= len q holds
q.(n+2) = f.[n,q.(n+1)]) & Z = q by A4,A49;
then Z.(n+2) = f.[n,Z.(n+1)] by A56,A60,NAT_1:8;
then p.(n+2) = f.[n,Z.(n+1)] by A61,FINSEQ_1:def 7;
hence thesis by A58,FINSEQ_1:def 7;
end;
n+2 = len Z + 1 implies thesis
proof
n+1+1 <= len Z + 1 by A55,FINSEQ_1:40;
then 1 <= n + 1 & n+1 <= len Z by NAT_1:12,XREAL_1:6;
then n+1 in Seg len Z by FINSEQ_1:1;
then
A62: n+1 in dom Z by FINSEQ_1:def 3;
assume
A63: n+2 = len Z + 1;
then p.(n+2) =<*f.[k,Z.(k+1)]*>.(n+2-(n+2-1 )) by A55,FINSEQ_1:23
.=f.[n,Z.(n+1)] by A52,A63;
hence thesis by A62,FINSEQ_1:def 7;
end;
hence thesis by A57;
end;
A64: p in D()*
proof
1 <= k + 1 by NAT_1:12;
then k+1 in Seg len Z by A52,FINSEQ_1:1;
then k+1 in dom Z by FINSEQ_1:def 3;
then
A65: Z.(k+1) in rng Z by FUNCT_1:def 3;
rng Z c= D() by FINSEQ_1:def 4;
then reconsider z=Z.(k+1) as Element of D() by A65;
reconsider n=k as Element of NAT by ORDINAL1:def 12;
p= Z^<*f.[n,z]*>;
hence thesis by FINSEQ_1:def 11;
end;
len p = len Z + len <*f.[k,Z.(k+1)]*> by FINSEQ_1:22
.=k+1+1 by A52,FINSEQ_1:39;
then k+1+1 in Seg len p by A51,FINSEQ_1:1;
then k+1+1 in dom p by FINSEQ_1:def 3;
then
A66: [k+1+1,p.(k+1+1)] in p by FUNCT_1:1;
ex p being FinSequence st p in D()* & p.1 = A() & (for n st n+2
<= len p holds p.(n+2) = f.[n,p.(n+1)]) & Z=p by A4,A49;
then p.1 = A() by A53,FINSEQ_1:def 7;
then p in X by A4,A64,A54;
then [k+1+1,p.(k+1+1)] in h by A38,A66,TARSKI:def 4;
hence thesis by FUNCT_1:1;
end;
k+1 <> len Z implies thesis
proof
k+1 in dom Z by A48,FUNCT_1:1;
then k+1 in Seg len Z by FINSEQ_1:def 3;
then
A67: k+1 <= len Z by FINSEQ_1:1;
assume k+1 <> len Z;
then k+1 < len Z by A67,XXREAL_0:1;
then
A68: k+1+1 <= len Z by NAT_1:13;
1 <= k+1+1 by NAT_1:12;
then k+1+1 in Seg len Z by A68,FINSEQ_1:1;
then k+1+1 in dom Z by FINSEQ_1:def 3;
then [k+1+1,Z.(k+1+1)] in Z by FUNCT_1:1;
then [k+1+1,Z.(k+1+1)] in h by A38,A49,TARSKI:def 4;
hence thesis by FUNCT_1:1;
end;
hence thesis by A50;
end;
[1,A()] in {[1,A()]} by TARSKI:def 1;
then [1,A()] in h by A38,A46,TARSKI:def 4;
then
A69: P[0] by FUNCT_1:1;
thus for k holds P[k] from NAT_1:sch 2(A69,A47);
end;
A70: for n holds h.(n+2) = f.[n,h.(n+1)]
proof
let n;
(n+1)+1 in dom h by A44;
then [n+2,h.(n+2)] in h by FUNCT_1:def 2;
then consider Z being set such that
A71: [n+2,h.(n+2)] in Z and
A72: Z in X by A38,TARSKI:def 4;
A73: ex p st p in D()* & (p.1=A() & for n st n+2 <= len p holds p.(n+2) =
f.[n,p.(n+1)]) & Z=p by A4,A72;
Z in D()* by A5,A72;
then reconsider Z as FinSequence of D() by FINSEQ_1:def 11;
n+2 in dom Z by A71,FUNCT_1:1;
then n+2 in Seg len Z by FINSEQ_1:def 3;
then
A74: n+2 <= len Z by FINSEQ_1:1;
n+1 <= n+2 by XREAL_1:7;
then 1 <= n+1 & n+1 <= len Z by A74,NAT_1:12,XXREAL_0:2;
then n+1 in Seg len Z by FINSEQ_1:1;
then n+1 in dom Z by FINSEQ_1:def 3;
then [n+1,Z.(n+1)] in Z by FUNCT_1:1;
then
A75: [n+1,Z.(n+1)] in h by A38,A72,TARSKI:def 4;
thus h.(n+2) = Z.(n+2) by A71,FUNCT_1:1
.= f.[n,Z.(n+1)] by A73,A74
.= f.[n,h.(n+1)] by A75,FUNCT_1:1;
end;
defpred P[object,object] means ex n st n = $1 & $2=h.(n+1);
A76: for x being object st x in NAT ex y being object st P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider n=x as Nat;
take h.(n+1);
take n;
thus thesis;
end;
consider g being Function such that
A77: dom g = NAT & for x being object st x in NAT holds P[x,g.x]
from CLASSES1:sch 1 (A76);
A78: dom g = NAT by A77;
A79: for n holds g.n = h.(n+1)
proof
let n;
n in NAT by ORDINAL1:def 12;
then ex m st m=n & g.n = h.(m+1) by A77;
hence thesis;
end;
rng g c= D()
proof
let x be object;
assume x in rng g;
then consider y being object such that
A80: y in dom g and
A81: x = g.y by FUNCT_1:def 3;
reconsider k=y as Nat by A78,A80;
k+1 in dom h by A44;
then
A82: h.(k+1) in rng h by FUNCT_1:def 3;
x=h.(k+1) by A79,A81;
hence thesis by A39,A82;
end;
then reconsider g as sequence of D() by A78,FUNCT_2:2;
A83: for n holds g.n = h.(n+1) by A79;
A84: for n st n + 2 <= len <*A()*> holds <*A()*>.(n+2) = f.[n,<*A()*>.(n+1) ]
proof
let n;
assume n + 2 <= len <*A()*>;
then n +1+1 <= 0 + 1 by FINSEQ_1:39;
then n + 1 <= 0 by XREAL_1:6;
then n + 1 <= 0 + n;
hence thesis by XREAL_1:6;
end;
<*A()*> in D()* & <*A()*>.1 = A() by FINSEQ_1:def 11;
then <*A()*> in X by A4,A84;
then
A85: {[1,A()]} in X by FINSEQ_1:37;
take g;
[1,A()] in {[1,A()]} by TARSKI:def 1;
then [1,A()] in h by A38,A85,TARSKI:def 4;
then A() = h.(0+1) by FUNCT_1:1
.= g.0 by A83;
hence g.0 = A();
let n be Nat;
A86: h.(n+(1+1)) =f.(n,h.(n+1)) by A70;
A87: n in NAT by ORDINAL1:def 12;
then g.n in D() by FUNCT_2:5;
then P[n,g.n,f.(n,g.n)] by A3,A87;
then P[n,g.n,h.(n+1+1)] by A83,A86;
hence thesis by A83;
end;
Lm2: 1 in REAL by NUMBERS:19;
scheme
FinRecEx{A() -> object,N() -> Nat,P[object,object,object]}:
ex p being FinSequence st
len p = N() & (p.1 = A() or N() = 0) & for n st 1 <= n & n < N() holds P[n,p.n,
p.(n+1)]
provided
A1: for n being Nat st 1 <= n & n < N() for x being set ex y
being set st P[n,x,y]
proof
defpred Q[Nat,set,set] means ($1 < N()-1 implies P[$1+1,$2,$3]) &
(not $1 < N()-1 implies $3=0);
A2: for n being Nat for x being set ex y being set st Q[n,x,y]
proof
let n be Nat,x be set;
n < N()-1 implies thesis
proof
assume
A3: n < N()-1;
then n+1 < N() by XREAL_1:20;
then consider y such that
A4: P[n+1,x,y] by A1,NAT_1:11;
take y;
thus n < N()-1 implies P[n+1,x,y] by A4;
thus thesis by A3;
end;
hence thesis;
end;
consider f being Function such that
A5: dom f = NAT & f.0 = A() & for n being Nat holds Q[n,f.n,f
.(n+1)] from RecEx(A2);
defpred Q[object,object] means
for r being Real st r=$1 holds $2=f.(r-1);
A6: for x being object st x in REAL ex y being object st Q[x,y]
proof
let x be object;
assume x in REAL;
then reconsider r=x as Real;
take f.(r-1);
thus thesis;
end;
consider g being Function such that
A7: dom g = REAL &
for x being object st x in REAL holds Q[x,g.x] from CLASSES1:sch
1(A6);
Seg N() c= REAL by NUMBERS:19;
then
A8: dom (g|Seg N()) = Seg N() by A7,RELAT_1:62;
then reconsider p = g|Seg N() as FinSequence by FINSEQ_1:def 2;
take p;
N() in NAT by ORDINAL1:def 12;
hence len p = N() by A8,FINSEQ_1:def 3;
N() <> 0 implies (p.1 = A() or N() = 0)
proof
assume N() <> 0;
then consider k being Nat such that
A9: N() = k+1 by NAT_1:6;
0 + 1 <= k +1 by XREAL_1:7;
then 1 in Seg N() by A9,FINSEQ_1:1;
then p.1 = g.1 by FUNCT_1:49
.= f.(1-1) by A7,Lm2
.= A() by A5;
hence thesis;
end;
hence p.1 = A() or N() = 0;
let n;
assume that
A10: 1 <= n and
A11: n < N();
0 <> n by A10;
then consider k being Nat such that
A12: n = k+1 by NAT_1:6;
A13: for n being Nat st n < N() holds p.(n+1) = f.n
proof
let n be Nat;
assume n < N();
then 1 <= n+1 & n+1 <= N() by NAT_1:11,13;
then
A14: n+1 in Seg N() by FINSEQ_1:1;
n+1 in REAL by XREAL_0:def 1;
then g.(n+1) = f.(n+1-1) by A7
.= f.n;
hence thesis by A14,FUNCT_1:49;
end;
reconsider k as Nat;
k <= k+1 by NAT_1:11;
then
A15: k < N() by A11,A12,XXREAL_0:2;
k < N()-1 by A11,A12,XREAL_1:20;
then P[k+1,f.k,f.(k+1)] by A5;
then P[k+1,f.k,p.(k+1+1)] by A13,A11,A12;
hence thesis by A13,A12,A15;
end;
scheme
FinRecExD{D() -> non empty set,A() -> Element of D(), N() -> Nat,
P[object,object,object]}:
ex p being FinSequence of D() st len p = N() & (p.1 = A() or N() = 0) &
for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)]
provided
A1: for n being Nat st 1 <= n & n < N() for x being Element
of D() ex y being Element of D() st P[n,x,y]
proof
set 00 = the Element of D();
defpred Z[Nat,set,set] means ($1 < N()-1 implies P[$1+1,$2,$3]) &
(not $1 < N()-1 implies $3=00);
A2: for n being Nat for x being Element of D() ex y being Element
of D() st Z[n,x,y]
proof
let n be Nat,x be Element of D();
n < N()-1 implies thesis
proof
assume
A3: n < N()-1;
then n+1 < N() by XREAL_1:20;
then consider y being Element of D() such that
A4: P[n+1,x,y] by A1,NAT_1:11;
take y;
thus n < N()-1 implies P[n+1,x,y] by A4;
thus thesis by A3;
end;
hence thesis;
end;
consider f being sequence of D() such that
A5: f.0 = A() & for n being Nat holds Z[n,f.n,f.(n+1)] from
RecExD(A2);
defpred P[object,object] means
for r being Real st r = $1 holds $2 = f.(r-1);
A6: for x being object st x in REAL ex y being object st P[x,y]
proof
let x be object;
assume x in REAL;
then reconsider r=x as Real;
take f.(r-1);
thus thesis;
end;
consider g being Function such that
A7: dom g = REAL &
for x being object st x in REAL holds P[x,g.x] from CLASSES1:sch
1(A6);
Seg N() c= REAL by NUMBERS:19;
then
A8: dom (g|Seg N()) = Seg N() by A7,RELAT_1:62;
then reconsider p = g|Seg N() as FinSequence by FINSEQ_1:def 2;
rng p c= D()
proof
let x be object;
assume x in rng p;
then consider y being object such that
A9: y in dom p and
A10: x = p.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A9;
A11: f.(y-1) in D()
proof
y <> 0 by A8,A9,FINSEQ_1:1;
then consider k being Nat such that
A12: y = k+1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
f.k in D();
hence thesis by A12;
end;
A13: y in REAL by XREAL_0:def 1;
p.y = g.y by A9,FUNCT_1:47;
hence thesis by A7,A10,A11,A13;
end;
then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
take p;
N() in NAT by ORDINAL1:def 12;
hence len p = N() by A8,FINSEQ_1:def 3;
N() <> 0 implies (p.1 = A() or N() = 0)
proof
assume N() <> 0;
then consider k being Nat such that
A14: N() = k+1 by NAT_1:6;
0 + 1 <= k +1 by XREAL_1:7;
then 1 in Seg N() by A14,FINSEQ_1:1;
then p.1 = g.1 by FUNCT_1:49
.= f.(1-1) by A7,Lm2
.= A() by A5;
hence thesis;
end;
hence p.1 = A() or N() = 0;
let n;
assume that
A15: 1 <= n and
A16: n < N();
0 <> n by A15;
then consider k being Nat such that
A17: n = k+1 by NAT_1:6;
A18: for n being Nat st n < N() holds p.(n+1) = f.n
proof
let n be Nat;
assume n < N();
then 1 <= n+1 & n+1 <= N() by NAT_1:11,13;
then
A19: n+1 in Seg N() by FINSEQ_1:1;
n+1 in REAL by XREAL_0:def 1;
then g.(n+1) = f.(n+1-1) by A7
.= f.n;
hence thesis by A19,FUNCT_1:49;
end;
reconsider k as Nat;
k <= k+1 by NAT_1:11;
then
A20: k < N() by A16,A17,XXREAL_0:2;
k < N() - 1 by A16,A17,XREAL_1:20;
then P[k+1,f.k,f.(k+1)] by A5;
then P[k+1,f.k,p.(k+1+1)] by A18,A16,A17;
hence thesis by A18,A17,A20;
end;
scheme
SeqBinOpEx{S() -> FinSequence,P[object,object,object]}:
ex x st ex p being
FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k
& k < len S() holds P[S().(k+1),p.k,p.(k+1)]
provided
A1: for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y]
proof
defpred Q[Nat,set,set] means P[S().($1+1),$2,$3];
A2: for k st 1 <= k & k < len S() for x ex y st Q[k,x,y] by A1;
consider p such that
A3: len p = len S() & (p.1 = S().1 or len S() = 0) & for k st 1 <= k & k
< len S() holds Q[k,p.k,p.(k+1)] from FinRecEx(A2);
A4: len S() <> 0 implies thesis
proof
assume
A5: len S() <> 0;
take p.(len p),p;
thus p.(len p) = p.(len p) & len p = len S() & p.1 = S().1 by A3,A5;
let k;
assume 1 <= k & k < len S();
hence thesis by A3;
end;
len S() = 0 implies thesis
proof
assume
A6: len S() = 0;
take S().0,S();
thus S().0 = S().(len S()) & len S() = len S() & S().1 = S(). 1 by A6;
thus thesis by A6;
end;
hence thesis by A4;
end;
scheme
LambdaSeqBinOpEx{S() -> FinSequence,F(object,object) -> set}:
ex x st ex p being
FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k
& k < len S() holds p.(k+1) = F(S().(k+1),p.k) proof
defpred P[object,object,object] means $3 = F($1,$2);
A1: for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y];
consider x such that
A2: ex p st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1
<= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] from SeqBinOpEx(A1);
take x;
consider p such that
A3: x = p.(len p) & len p = len S() & p.1 = S().1 and
A4: for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k) by A2;
take p;
thus x = p.(len p) & len p = len S() & p.1 = S().1 by A3;
let k;
assume 1 <= k & k < len S();
hence thesis by A4;
end;
:: Schemes of uniqueness
scheme
FinRecUn{A() -> object, N() -> Nat, F,G() -> FinSequence,
P[object,object,object]}:
F() = G()
provided
A1: for n st 1 <= n & n < N() for x,y1,y2 being set st P[n,x,y1] & P[n,x
,y2] holds y1 = y2 and
A2: len F() = N() & (F().1 = A() or N() = 0) & for n st 1 <= n & n < N()
holds P[n,F().n,F().(n+1)] and
A3: len G() = N() & (G().1 = A() or N() = 0) & for n st 1 <= n & n < N()
holds P[n,G().n,G().(n+1)]
proof
defpred P[Nat] means 1 <= $1 & $1 <= N() & F().$1 <> G().$1;
assume
A4: F() <> G();
dom F() = Seg len G() by A2,A3,FINSEQ_1:def 3
.= dom G() by FINSEQ_1:def 3;
then consider x being object such that
A5: x in dom F() and
A6: F().x <> G().x by A4;
A7: x in Seg len F() by A5,FINSEQ_1:def 3;
reconsider x as Nat by A5;
A8: 1 <= x by A7,FINSEQ_1:1;
x <= N() by A2,A7,FINSEQ_1:1;
then
A9: ex n be Nat st P[n] by A6,A8;
consider n be Nat such that
A10: P[n]& for k be Nat st P[k] holds n <= k from NAT_1:sch 5(A9);
0 <> n by A10;
then consider k being Nat such that
A11: n = k+1 by NAT_1:6;
reconsider k as Nat;
n <> 1 by A2,A3,A10;
then 1 < n by A10,XXREAL_0:1;
then
A12: 1 <= k by A11,NAT_1:13;
k < n by A11,XREAL_1:29;
then
A13: k < N() by A10,XXREAL_0:2;
n > k by A11,NAT_1:13;
then F().k = G().k by A10,A12,A13;
then
A14: P[k,F().k,G().(k+1)] by A3,A12,A13;
P[k,F().k,F().(k+1)] by A2,A12,A13;
hence contradiction by A1,A10,A11,A12,A13,A14;
end;
scheme
FinRecUnD{D() -> non empty set, A() -> Element of D(), N() -> Nat, F, G() ->
FinSequence of D(), P[object,object,object]}: F() = G()
provided
A1: for n st 1 <= n & n < N() for x,y1,y2 being Element of D() st P[n,x,
y1] & P[n,x,y2] holds y1 = y2 and
A2: len F() = N() & (F().1 = A() or N() = 0) & for n st 1 <= n & n < N()
holds P[n,F().n,F().(n+1)] and
A3: len G() = N() & (G().1 = A() or N() = 0) & for n st 1 <= n & n < N()
holds P[n,G().n,G().(n+1)]
proof
defpred P[Nat] means 1 <= $1 & $1 <= N() & F().$1 <> G().$1;
assume
A4: F() <> G();
dom F() = Seg len G() by A2,A3,FINSEQ_1:def 3
.= dom G() by FINSEQ_1:def 3;
then consider x being object such that
A5: x in dom F() and
A6: F().x <> G().x by A4;
A7: x in Seg len F() by A5,FINSEQ_1:def 3;
reconsider x as Nat by A5;
A8: 1 <= x by A7,FINSEQ_1:1;
x <= N() by A2,A7,FINSEQ_1:1;
then
A9: ex n be Nat st P[n] by A6,A8;
consider n be Nat such that
A10: P[n] & for k be Nat st P[k] holds n <= k from NAT_1:sch 5(A9);
0 <> n by A10;
then consider k being Nat such that
A11: n = k+1 by NAT_1:6;
reconsider k as Nat;
reconsider Gk1 = G().(k+1) as Element of D() by A3,A10,A11,Lm1;
n <> 1 by A2,A3,A10;
then 1 < n by A10,XXREAL_0:1;
then
A12: 1 <= k by A11,NAT_1:13;
k < n by A11,XREAL_1:29;
then
A13: k < N() by A10,XXREAL_0:2;
then reconsider Fk = F().k as Element of D() by A2,A12,Lm1;
n > k by A11,NAT_1:13;
then F().k = G().k by A10,A12,A13;
then
A14: P[k,Fk,Gk1] by A3,A12,A13;
reconsider Fk1 = F().(k+1) as Element of D() by A2,A10,A11,Lm1;
P[k,Fk,Fk1] by A2,A12,A13;
hence contradiction by A1,A10,A11,A12,A13,A14;
end;
scheme
SeqBinOpUn{S() -> FinSequence,P[object,object,object], x,y() -> object}:
x() = y()
provided
A1: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1]
& P[z,x,y2] holds y1 = y2 and
A2: ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 =
S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] and
A3: ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 =
S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)]
proof
defpred Q[Nat,set,set] means P[S().($1+1),$2,$3];
A4: for k st 1 <= k & k < len S() for x,y1,y2 st Q[k,x,y1] & Q[k,x,y2] holds
y1 = y2 by A1;
consider q such that
A5: y() = q.(len q) and
A6: len q = len S() & q.1 = S().1 & for k st 1 <= k & k < len S() holds
Q[k, q.k,q.(k+1)] by A3;
A7: len q = len S() & (q.1 = S().1 or len S() = 0) & for k st 1 <= k & k <
len S() holds Q[k,q.k,q.(k+1)] by A6;
consider p such that
A8: x() = p.(len p) and
A9: len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds
Q[k, p.k,p.(k+1)] by A2;
A10: len p = len S() & (p.1 = S().1 or len S() = 0) & for k st 1 <= k & k <
len S() holds Q[k,p.k,p.(k+1)] by A9;
p = q from FinRecUn(A4,A10,A7);
hence thesis by A8,A5;
end;
scheme
LambdaSeqBinOpUn{S() -> FinSequence, F(object,object) -> object,
x, y() -> object}:
x() = y()
provided
A1: ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 =
S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k) and
A2: ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 =
S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k)
proof
defpred P[set,set,set] means $3 = F($1,$2);
A3: ex p st y() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <=
k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] by A2;
A4: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1] & P[
z,x,y2] holds y1 = y2;
A5: ex p st x() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <=
k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] by A1;
thus x() = y() from SeqBinOpUn(A4,A5,A3);
end;
:: Schemes of definitness
scheme
DefRec{A() -> object,n() -> Nat,P[object,object,object]}:
(ex y being set st ex f being
Function st y = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)])
& for y1,y2 being set st (ex f being Function st y1 = f.n() & dom f = NAT & f.0
= A() & for n holds P[n,f.n,f.(n+1)]) & (ex f being Function st y2 = f.n() &
dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) holds y1 = y2
provided
A1: for n,x ex y st P[n,x,y] and
A2: for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
A3: for n,x ex y st P[n,x,y] by A1;
consider f being Function such that
A4: dom f = NAT & f.0 = A() & for n being Nat holds P[n,f.n,f
.(n+1)] from RecEx(A3);
A5: for n being Nat,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2
by A2;
thus ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0
= A() & for n holds P[n,f.n,f.(n+1)]
proof
take f.n(),f;
thus thesis by A4;
end;
let y1,y2 be set;
given f1 being Function such that
A6: y1 = f1.n() and
A7: dom f1 = NAT and
A8: f1.0 = A() and
A9: for n holds P[n,f1.n,f1.(n+1)];
A10: for n being Nat holds P[n,f1.n,f1.(n+1)]
by A9;
given f2 being Function such that
A11: y2 = f2.n() and
A12: dom f2 = NAT and
A13: f2.0 = A() and
A14: for n holds P[n,f2.n,f2.(n+1)];
A15: for n being Nat holds P[n,f2.n,f2.(n+1)] by A14;
f1 = f2 from NAT_1:sch 13(A7,A8,A10,A12,A13,A15,A5);
hence thesis by A6,A11;
end;
scheme
LambdaDefRec{A() -> object,n() -> Nat,RecFun(object,object) -> set}:
(ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0 = A()
& for n holds f.(
n+1) = RecFun(n,f.n)) & for y1,y2 being set st (ex f being Function st y1 = f.n
() & dom f = NAT & f.0 = A() & for n holds f.(n+1) = RecFun(n,f.n)) & (ex f
being Function st y2 = f.n() & dom f = NAT & f.0 = A() & for n holds f.(n+1) =
RecFun(n,f.n)) holds y1 = y2 proof
defpred P[set,set,set] means for z st z = $2 holds $3 = RecFun($1,z);
A1: for n,x ex y st P[n,x,y]
proof
let n,x;
take RecFun(n,x);
thus thesis;
end;
A2: for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2
proof
let n,x,y1,y2;
assume that
A3: for z st z = x holds y1 = RecFun(n,z) and
A4: for z st z = x holds y2 = RecFun(n,z);
thus y1 = RecFun(n,x) by A3
.= y2 by A4;
end;
A5: (ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0
= A() & for n holds P[n,f.n,f.(n+1)] ) & for y1,y2 being set st (ex f being
Function st y1 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]
) & (ex f being Function st y2 = f.n() & dom f = NAT & f.0 = A() & for n holds
P[n,f.n,f.(n+1)] ) holds y1 = y2 from DefRec(A1,A2);
then consider y being set, f being Function such that
A6: y = f.n() & dom f = NAT &( f.0 = A() & for n holds P[n,f.n,f.(n+1)] );
thus ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0
= A() & for n holds f.(n+1) = RecFun(n,f.n)
proof
take y,f;
thus thesis by A6;
end;
let y1,y2 being set;
given f1 being Function such that
A7: y1 = f1.n() & dom f1 = NAT & f1.0 = A() and
A8: for n holds f1.(n+1) = RecFun(n,f1.n);
A9: for n holds P[n,f1.n,f1.(n+1)] by A8;
given f2 being Function such that
A10: y2 = f2.n() & dom f2 = NAT & f2.0 = A() and
A11: for n holds f2.(n+1) = RecFun(n,f2.n);
for n holds P[n,f2.n,f2.(n+1)] by A11;
hence thesis by A5,A7,A10,A9;
end;
scheme
DefRecD{D() -> non empty set,A() -> (Element of D()), n() -> Nat,
P[object,object,object]}:
(ex y being Element of D() st ex f being sequence of D() st y = f.n(
) & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) & for y1,y2 being Element of D()
st (ex f being sequence of D() st y1 = f.n() & f.0 = A() & for n holds P[n,
f.n,f.(n+1)]) & (ex f being sequence of D() st y2 = f.n() & f.0 = A() & for
n holds P[n,f.n,f.(n+1)]) holds y1 = y2
provided
A1: for n being Nat,x being Element of D() ex y being Element
of D() st P[n,x,y] and
A2: for n being Nat, x,y1,y2 being Element of D() st P[n,x,y1
] & P[n,x,y2] holds y1 = y2
proof
A3: for n being Nat,x being Element of D() ex y being Element of
D() st P[n,x,y] by A1;
consider f being sequence of D() such that
A4: f.0 = A() & for n being Nat holds P[n,f.n,f.(n+1)] from
RecExD(A3);
A5: for n being Nat, x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2]
holds y1 = y2
by A2;
thus ex y being Element of D() st ex f being sequence of D() st y = f.n(
) & f.0 = A() & for n holds P[n,f.n,f.(n+1)]
proof
reconsider n = n() as Element of NAT by ORDINAL1:def 12;
take f.n,f;
thus thesis by A4;
end;
let y1,y2 be Element of D();
given f1 being sequence of D() such that
A6: y1 = f1.n() and
A7: f1.0 = A() and
A8: for n holds P[n,f1.n,f1.(n+1)];
A9: f1.0 = A() by A7;
A10: for n being Nat holds P[n,f1.n,f1.(n+1)]
by A8;
given f2 being sequence of D() such that
A11: y2 = f2.n() and
A12: f2.0 = A() and
A13: for n holds P[n,f2.n,f2.(n+1)];
A14: for n being Nat holds P[n,f2.n,f2.(n+1)]
by A13;
A15: f2.0 = A() by A12;
f1 = f2 from NAT_1:sch 14(A9,A10,A15,A14,A5);
hence thesis by A6,A11;
end;
scheme
LambdaDefRecD{D() -> non empty set, A() -> Element of D(), n() -> Nat,
RecFun(object,object) -> Element of D()}:
(ex y being Element of D() st ex f being
sequence of D() st y = f.n() & f.0 = A() & for n being Nat holds f.(n+1) =
RecFun(n,f.n)) & for y1,y2 being Element of D() st (ex f being sequence of
D() st y1 = f.n() & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n))
& (ex f being sequence of D() st y2 = f.n() & f.0 = A() & for n being Nat
holds f.(n+1) = RecFun(n,f.n)) holds y1 = y2 proof
defpred Q[set,set,set] means for z being Element of D() st z=$2 holds $3 =
RecFun($1,z);
A1: for n being Nat,x being Element of D() ex y being Element of
D() st Q[n,x,y]
proof
let n be Nat,x be Element of D();
take RecFun(n,x);
let z be Element of D();
assume z = x;
hence thesis;
end;
A2: for n being Nat,x,y1,y2 being Element of D() st Q[n,x,y1] & Q
[n,x,y2] holds y1 = y2
proof
let n be Nat,x,y1,y2 be Element of D();
assume that
A3: for z being Element of D() st z = x holds y1 = RecFun(n,z) and
A4: for z being Element of D() st z = x holds y2 = RecFun(n,z);
thus y1 = RecFun(n,x) by A3
.= y2 by A4;
end;
A5: (ex y being Element of D() st ex f being sequence of D() st y = f.n(
) & f.0 = A() & for n being Nat holds Q[n,f.n,f.(n+1)]) & for y1,y2
being Element of D() st (ex f being sequence of D() st y1 = f.n() & f.0 = A
() & for n being Nat holds Q[n,f.n,f.(n+1)]) & (ex f being sequence of D()
st y2 = f.n() & f.0 = A() & for n being Nat holds Q[n,f.n
,f.(n+1)]) holds y1 = y2 from DefRecD(A1,A2);
then consider y being Element of D(), f being sequence of D() such that
A6: y = f.n() & f.0 = A() and
A7: for n being Nat holds Q[n,f.n,f.(n+1)];
thus ex y being Element of D() st ex f being sequence of D() st y = f.n(
) & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n)
proof
take y,f;
thus y = f.n() & f.0 = A() by A6;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
Q[n,f.n,f.(n+1)] by A7;
hence thesis;
end;
let y1,y2 being Element of D();
given f being sequence of D() such that
A8: y1 = f.n() & f.0 = A() and
A9: for n being Nat holds f.(n+1) = RecFun(n,f.n);
A10: for n being Nat holds Q[n,f.n,f.(n+1)] by A9;
given f2 being sequence of D() such that
A11: y2 = f2.n() & f2.0 = A() and
A12: for n being Nat holds f2.(n+1) = RecFun(n,f2.n);
for n being Nat holds Q[n,f2.n,f2.(n+1)] by A12;
hence thesis by A5,A8,A11,A10;
end;
scheme
SeqBinOpDef{S() -> FinSequence,P[object,object,object]}:
(ex x st ex p being
FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k
& k < len S() holds P[S().(k+1),p.k,p.(k+1)]) & for x,y st (ex p being
FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k
& k < len S() holds P[S().(k+1),p.k,p.(k+1)]) & (ex p being FinSequence st y =
p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds
P[S().(k+1),p.k,p.(k+1)]) holds x = y
provided
A1: for k,y st 1 <= k & k < len S() ex z st P[S().(k+1),y,z] and
A2: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1]
& P[z,x,y2] holds y1 = y2
proof
A3: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1] & P[
z,x,y2] holds y1 = y2 by A2;
A4: for k,y st 1 <= k & k < len S() ex z st P[S().(k+1),y,z] by A1;
thus ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1
= S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] from
SeqBinOpEx(A4);
let x,y;
assume
A5: ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S(
).1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)];
assume
A6: ex p being FinSequence st y = p.(len p) & len p = len S() & p.1 = S(
).1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)];
thus x = y from SeqBinOpUn(A3,A5,A6);
end;
scheme
LambdaSeqBinOpDef{S() -> FinSequence,F(object,object) -> set}:
(ex x st ex p being
FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k
& k < len S() holds p.(k+1) = F(S().(k+1),p.k)) & for x,y st (ex p being
FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k
& k < len S() holds p.(k+1) = F(S().(k+1),p.k)) & (ex p being FinSequence st y
= p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S()
holds p.(k+1) = F(S().(k+1),p.k)) holds x = y proof
thus ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1
= S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k) from
LambdaSeqBinOpEx;
let x,y;
assume
A1: ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S(
).1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k);
assume
A2: ex p being FinSequence st y = p.(len p) & len p = len S() & p.1 = S(
).1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k);
thus x = y from LambdaSeqBinOpUn(A1,A2);
end;
:: from POLYNOM2, 2010.02.13, A.T.
scheme
SeqExD{D() -> non empty set, N() -> Nat, P[object,object]}: ex p being
FinSequence of D() st dom p = Seg N() & for k being Nat st k in Seg
N() holds P[k,p/.k]
provided
A1: for k being Nat st k in Seg N() ex x being Element of D()
st P[k,x]
proof
per cases;
suppose
A2: N() = 0;
take <*>(D());
thus thesis by A2;
end;
suppose
A3: N() <> 0;
now
assume
A4: Seg N() = {};
now
per cases;
case
N() = 0;
hence contradiction by A3;
end;
case
N() <> 0;
hence contradiction by A4;
end;
end;
hence contradiction;
end;
then reconsider M = Seg N() as non empty set;
A5: for x being Element of M ex y being Element of D() st P[x,y]
proof
let x be Element of M;
x in Seg N();
hence thesis by A1;
end;
consider f being Function of M,D() such that
A6: for x being Element of M holds P[x,f.x] from FUNCT_2:sch 3(A5);
dom f = Seg N() by FUNCT_2:def 1;
then reconsider q = f as FinSequence by FINSEQ_1:def 2;
now
let u be object;
A7: rng q c= D() by RELAT_1:def 19;
assume u in rng q;
hence u in D() by A7;
end;
then rng q c= D();
then reconsider q as FinSequence of D() by FINSEQ_1:def 4;
take q;
now
let k be Nat;
assume
A8: k in Seg N();
then k in dom q by FUNCT_2:def 1;
then q.k = q/.k by PARTFUN1:def 6;
hence P[k,q/.k] by A6,A8;
end;
hence thesis by FUNCT_2:def 1;
end;
end;
scheme
FinRecExD2{D() -> non empty set,A() -> (Element of D()), N() -> Element of
NAT, P[object,object,object]}:
ex p being FinSequence of D() st len p = N() & (p/.1 = A(
) or N() = 0) & for n being Nat st 1 <= n & n <= N()-1 holds P[n,p/.
n,p/.(n+1)]
provided
A1: for n being Nat st 1 <= n & n <= N()-1 holds for x being
Element of D() ex y being Element of D() st P[n,x,y]
proof
set 00 = the Element of D();
defpred Q[Nat,set,set] means (0 <= $1 & $1 <= N()-2 implies P[$1+
1,$2,$3]) & (not (0 <= $1 & $1 <= N()-2) implies $3=00);
A2: for n be Nat for x be Element of D() ex y be Element of D()
st Q[n,x,y]
proof
let n be Nat,x be Element of D();
0 <= n & n <= N()-2 implies thesis
proof
A3: 0+1 <= n+1 by XREAL_1:6;
assume that
0 <= n and
A4: n <= N()-2;
n+1 <= N()-2+1 by A4,XREAL_1:6;
then consider y being Element of D() such that
A5: P[n+1,x,y] by A1,A3;
take y;
thus 0 <= n & n <= N()-2 implies P[n+1,x,y] by A5;
thus thesis by A4;
end;
hence thesis;
end;
consider f being sequence of D() such that
A6: f.0 = A() & for n being Nat holds Q[n,f.n,f.(n+1)]
from RecExD(A2);
defpred Q[object,object] means
for r being Real st r = $1 holds $2 = f.(r-1);
A7: for x being object st x in REAL ex y being object st Q[x,y]
proof
let x be object;
assume x in REAL;
then reconsider r=x as Real;
take f.(r-1);
thus thesis;
end;
consider g being Function such that
A8: dom g = REAL & for x being object st x in REAL holds Q[x,g.x] from
CLASSES1:sch 1(A7);
Seg N() c= REAL by NUMBERS:19;
then
A9: dom (g|Seg N()) = Seg N() by A8,RELAT_1:62;
then reconsider p = g|Seg N() as FinSequence by FINSEQ_1:def 2;
now
let x be object;
assume x in rng p;
then consider y being object such that
A10: y in dom p and
A11: x = p.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A10;
A12: f.(y-1) in D()
proof
y <> 0 by A9,A10,FINSEQ_1:1;
then consider k being Nat such that
A13: y = k+1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
f.k in D();
hence thesis by A13;
end;
A14: y in REAL by XREAL_0:def 1;
p.y = g.y by A10,FUNCT_1:47;
hence x in D() by A8,A11,A12,A14;
end;
then rng p c= D();
then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
take p;
thus len p = N() by A9,FINSEQ_1:def 3;
N() <> 0 implies p/.1 = A()
proof
assume N() <> 0;
then consider k being Nat such that
A15: N() = k+1 by NAT_1:6;
0 + 1 <= k +1 by XREAL_1:7;
then
A16: 1 in Seg N() by A15,FINSEQ_1:1;
then p/.1 = p.1 by A9,PARTFUN1:def 6
.= g.1 by A16,FUNCT_1:49
.= f.(1-1) by A8,Lm2
.= A() by A6;
hence thesis;
end;
hence p/.1 = A() or N() = 0;
let n be Nat;
assume that
A17: 1 <= n and
A18: n <= N()-1;
consider k being Nat such that
A19: n = k+1 by A17,NAT_1:6;
A20: for n being Nat st n <= N()-1 holds p/.(n+1) = f.n
proof
let n be Nat;
assume n <= N() - 1;
then
A21: n+1 <= N()-1+1 by XREAL_1:6;
n+1 in REAL by XREAL_0:def 1;
then
A22: g.(n+1) = f.(n+1-1) by A8
.= f.n;
1 <= n+1 by NAT_1:11;
then
A23: n+1 in Seg N() by A21,FINSEQ_1:1;
then p/.(n+1) = p.(n+1) by A9,PARTFUN1:def 6;
hence thesis by A23,A22,FUNCT_1:49;
end;
A24: k <= k+1 by NAT_1:11;
k <= N()-1-1 by A18,A19,XREAL_1:19;
then P[k+1,f.k,f.(k+1)] by A6;
then P[k+1,f.k,p/.(k+1+1)] by A20,A18,A19;
hence thesis by A20,A18,A19,A24,XXREAL_0:2;
end;