:: RECDEF_1 semantic presentation

begin

            Lm1:  for n being Element of NAT
for D being non empty set
for p being FinSequence of D st 1 <= n & n <= len p holds
p . n is Element of D
proof
let n be Element of NAT ; ::_thesis: for D being non empty set
for p being FinSequence of D st 1 <= n & n <= len p holds
p . n is Element of D
let D be non empty set ; ::_thesis: for p being FinSequence of D st 1 <= n & n <= len p holds
p . n is Element of D
let p be FinSequence of D; ::_thesis: ( 1 <= n & n <= len p implies p . n is Element of D )
assume  ( 1 <= n & n <= len p ) ; ::_thesis: p . n is Element of D
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  p . n is Element of D by A1; ::_thesis: verum
end;

definition
let p be natural-valued Function;
let n be set ;
:: original: .
redefine funcp . n ->  Element of NAT ;
coherence
 p . n is Element of NAT by ORDINAL1:def_12;
end;

scheme :: RECDEF_1:sch 1
RecEx{ F1() ->  set , P1[ set , set , set ] } :
 ex f being Function st
( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
provided
A1: for n being Element of NAT
for x being set ex y being set st P1[n,x,y]
proof
defpred S1[ set , set , set ] means  ex O2 being Ordinal st
( O2 = $3 & ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of $2) holds
ex Y being set st
( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of $2) holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O2 c= O ) );
A2: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
defpred S2[ set , set ] means  for m being Element of NAT ex y being set st
( $2 is Ordinal & y c= Rank (the_rank_of $2) & P1[m,$1,y] );
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; ::_thesis: ex y being set st S1[n,x,y]
defpred S3[ Ordinal] means  for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank $1 & P1[n,X,Y] );
A3: for x9 being set st x9 in bool (Rank (the_rank_of x)) holds
ex o being set st S2[x9,o]
proof
let x9 be set ; ::_thesis: ( x9 in bool (Rank (the_rank_of x)) implies ex o being set st S2[x9,o] )
assume  x9 in bool (Rank (the_rank_of x)) ; ::_thesis: ex o being set st S2[x9,o]
defpred S4[ set , set ] means  ex y being set st
( $2 is Ordinal & y c= Rank (the_rank_of $2) & P1[$1,x9,y] );
A4: for e being set st e in NAT holds
ex u being set st S4[e,u]
proof
let i be set ; ::_thesis: ( i in NAT implies ex u being set st S4[i,u] )
assume  i in NAT ; ::_thesis: ex u being set st S4[i,u]
then reconsider i9 = i as Element of NAT ;
thus  ex o, y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] ) ::_thesis: verum
proof
consider y being set  such that
A5: P1[i9,x9,y] by A1;
take o = the_rank_of y; ::_thesis: ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] )
take  y ; ::_thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P1[i,x9,y] )
thus  o is Ordinal ; ::_thesis: ( y c= Rank (the_rank_of o) & P1[i,x9,y] )
 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; ::_thesis: P1[i,x9,y]
thus  P1[i,x9,y] by A5; ::_thesis: verum
end;
end;
consider h being Function such that
A6: dom h = NAT and
A7: for i being set st i in NAT holds
S4[i,h . i] from CLASSES1:sch_1(A4);
take o = sup (rng h); ::_thesis: S2[x9,o]
thus  for m being Element of NAT ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] ) ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ex y being set st
( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] )
consider y being set  such that
A8: h . m is Ordinal and
A9: y c= Rank (the_rank_of (h . m)) and
A10: P1[m,x9,y] by A7;
reconsider O = h . m as Ordinal by A8;
 h . m in rng h by A6, FUNCT_1:def_3;
then  h . m in sup (rng h) by A8, ORDINAL2:19;
then  h . m c= o by ORDINAL1:def_2;
then A11: Rank O c= Rank o by CLASSES1:37;
take  y ; ::_thesis: ( o is Ordinal & y c= Rank (the_rank_of o) & P1[m,x9,y] )
thus  o is Ordinal ; ::_thesis: ( y c= Rank (the_rank_of o) & P1[m,x9,y] )
 y c= Rank O by A9, CLASSES1:73;
then  y c= Rank o by A11, XBOOLE_1:1;
hence  y c= Rank (the_rank_of o) by CLASSES1:73; ::_thesis: P1[m,x9,y]
thus  P1[m,x9,y] by A10; ::_thesis: verum
end;
end;
consider f being Function such that
A12: dom f = bool (Rank (the_rank_of x)) and
A13: for x9 being set st x9 in bool (Rank (the_rank_of x)) holds
S2[x9,f . x9] from CLASSES1:sch_1(A3);
A14: ex O being Ordinal st S3[O]
proof
take O2 = sup (rng f); ::_thesis: S3[O2]
thus  for X being set
for m being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] ) ::_thesis: verum
proof
let X be set ; ::_thesis: for m being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] )
let m be Element of NAT ; ::_thesis: ( X c= Rank (the_rank_of x) implies ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] ) )
assume A15: X c= Rank (the_rank_of x) ; ::_thesis: ex Y being set st
( Y c= Rank O2 & P1[m,X,Y] )
then consider Y being set  such that
A16: f . X is Ordinal and
A17: Y c= Rank (the_rank_of (f . X)) and
A18: P1[m,X,Y] by A13;
reconsider O = f . X as Ordinal by A16;
 f . X in rng f by A12, A15, FUNCT_1:def_3;
then  f . X in sup (rng f) by A16, ORDINAL2:19;
then  f . X c= O2 by ORDINAL1:def_2;
then A19: Rank O c= Rank O2 by CLASSES1:37;
take  Y ; ::_thesis: ( Y c= Rank O2 & P1[m,X,Y] )
 the_rank_of O = O by CLASSES1:73;
hence  Y c= Rank O2 by A17, A19, XBOOLE_1:1; ::_thesis: P1[m,X,Y]
thus  P1[m,X,Y] by A18; ::_thesis: verum
end;
end;
consider O2 being Ordinal such that
A20: ( S3[O2] & ( for O being Ordinal st S3[O] holds
O2 c= O ) ) from ORDINAL1:sch_1(A14);
take  O2 ; ::_thesis: S1[n,x,O2]
thus  S1[n,x,O2] by A20; ::_thesis: verum
end;
A21: for n being Element of NAT
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be Element of NAT ; ::_thesis: for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
let x, y1, y2 be set ; ::_thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that
A22: S1[n,x,y1] and
A23: S1[n,x,y2] ; ::_thesis: y1 = y2
consider O2 being Ordinal such that
A24: O2 = y2 and
A25: ( ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O2 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O2 c= O ) ) by A23;
consider O1 being Ordinal such that
A26: O1 = y1 and
A27: ( ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O1 & P1[n,X,Y] ) ) & ( for O being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of x) holds
ex Y being set st
( Y c= Rank O & P1[n,X,Y] ) ) holds
O1 c= O ) ) by A22;
 ( O1 c= O2 & O2 c= O1 ) by A27, A25;
hence  y1 = y2 by A26, A24, XBOOLE_0:def_10; ::_thesis: verum
end;
 ex f being Function st
( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) )
proof
deffunc H1( Element of NAT ) ->  set =  {  k where k is Element of NAT : k <= $1  }  ;
A28: for p, q being Function
for k being Element of NAT st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Element of NAT st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds
p . k = q . k
proof
let p, q be Function; ::_thesis: for k being Element of NAT st dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Element of NAT st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) holds
p . k = q . k
let k be Element of NAT ; ::_thesis: ( dom p = H1(k) & dom q = H1(k + 1) & p . 0 = q . 0 & ( for n being Element of NAT st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ) implies p . k = q . k )
defpred S2[ Element of NAT ] means ( $1 <= k implies p . $1 = q . $1 );
assume that
 dom p = H1(k) and
 dom q = H1(k + 1) and
A29: p . 0 = q . 0 and
A30: for n being Element of NAT st n < k holds
( S1[n,p . n,p . (n + 1)] & S1[n,q . n,q . (n + 1)] ) ; ::_thesis: p . k = q . k
A31: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A32: ( n <= k implies p . n = q . n ) ; ::_thesis: S2[n + 1]
assume  n + 1 <= k ; ::_thesis: p . (n + 1) = q . (n + 1)
then A33: n < k by NAT_1:13;
then A34: S1[n,p . n,p . (n + 1)] by A30;
 S1[n,p . n,q . (n + 1)] by A30, A32, A33;
hence  p . (n + 1) = q . (n + 1) by A21, A34; ::_thesis: verum
end;
A35: S2[ 0 ] by A29;
 for n being Element of NAT holds S2[n] from NAT_1:sch_1(A35, A31);
hence  p . k = q . k ; ::_thesis: verum
end;
A36: for n being Element of NAT ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) )
proof
defpred S2[ Element of NAT ] means  ex p being Function st
( dom p = H1($1) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < $1 holds
S1[k,p . k,p . (k + 1)] ) );
A37: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
given p being Function such that  dom p = H1(n) and
A38: p . 0 = the_rank_of F1() and
A39: for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ; ::_thesis: S2[n + 1]
consider z being set  such that
A40: S1[n,p . n,z] by A2;
defpred S3[ set , set ] means  for k being Element of NAT st k = $1 holds
( ( k <= n implies $2 = p . k ) & ( k = n + 1 implies $2 = z ) );
A41: for x being set st x in H1(n + 1) holds
ex y being set st S3[x,y]
proof
let x be set ; ::_thesis: ( x in H1(n + 1) implies ex y being set st S3[x,y] )
assume  x in H1(n + 1) ; ::_thesis: ex y being set st S3[x,y]
then A42: ex m being Element of NAT st
( m = x & m <= n + 1 ) ;
then reconsider t = x as Element of NAT ;
A43: ( t <= n implies ex y being set st S3[x,y] )
proof
assume A44: t <= n ; ::_thesis: ex y being set st S3[x,y]
take  p . x ; ::_thesis: S3[x,p . x]
let k be Element of NAT ; ::_thesis: ( k = x implies ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) ) )
assume A45: k = x ; ::_thesis: ( ( k <= n implies p . x = p . k ) & ( k = n + 1 implies p . x = z ) )
hence  ( k <= n implies p . x = p . k ) ; ::_thesis: ( k = n + 1 implies p . x = z )
assume  k = n + 1 ; ::_thesis: p . x = z
then  n + 1 <= n + 0 by A44, A45;
hence  p . x = z by XREAL_1:6; ::_thesis: verum
end;
 ( t = n + 1 implies ex y being set st S3[x,y] )
proof
assume A46: t = n + 1 ; ::_thesis: ex y being set st S3[x,y]
take  z ; ::_thesis: S3[x,z]
let k be Element of NAT ; ::_thesis: ( k = x implies ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) ) )
assume A47: k = x ; ::_thesis: ( ( k <= n implies z = p . k ) & ( k = n + 1 implies z = z ) )
thus  ( k <= n implies z = p . k ) ::_thesis: ( k = n + 1 implies z = z )
proof
assume  k <= n ; ::_thesis: z = p . k
then  n + 1 <= n + 0 by A46, A47;
hence  z = p . k by XREAL_1:6; ::_thesis: verum
end;
thus  ( k = n + 1 implies z = z ) ; ::_thesis: verum
end;
hence  ex y being set st S3[x,y] by A42, A43, NAT_1:8; ::_thesis: verum
end;
consider q being Function such that
A48: ( dom q = H1(n + 1) & ( for x being set st x in H1(n + 1) holds
S3[x,q . x] ) ) from CLASSES1:sch_1(A41);
take  q ; ::_thesis: ( dom q = H1(n + 1) & q . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n + 1 holds
S1[k,q . k,q . (k + 1)] ) )
thus  dom q = H1(n + 1) by A48; ::_thesis: ( q . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n + 1 holds
S1[k,q . k,q . (k + 1)] ) )
 0 in H1(n + 1) ;
hence  q . 0 = the_rank_of F1() by A38, A48; ::_thesis: for k being Element of NAT st k < n + 1 holds
S1[k,q . k,q . (k + 1)]
let k be Element of NAT ; ::_thesis: ( k < n + 1 implies S1[k,q . k,q . (k + 1)] )
assume A49: k < n + 1 ; ::_thesis: S1[k,q . k,q . (k + 1)]
A50: now__::_thesis:_(_k_<>_n_implies_S1[k,q_._k,q_._(k_+_1)]_)
A51: k + 1 <= n + 1 by A49, NAT_1:13;
assume  k <> n ; ::_thesis: S1[k,q . k,q . (k + 1)]
then  k + 1 <> n + 1 ;
then A52: k + 1 <= n by A51, NAT_1:8;
then A53: k < n by NAT_1:13;
 k + 1 in H1(n + 1) by A51;
then A54: q . (k + 1) = p . (k + 1) by A48, A52;
 k in H1(n + 1) by A49;
then  p . k = q . k by A48, A53;
hence  S1[k,q . k,q . (k + 1)] by A39, A54, A53; ::_thesis: verum
end;
now__::_thesis:_(_k_=_n_implies_S1[k,q_._k,q_._(k_+_1)]_)
assume A55: k = n ; ::_thesis: S1[k,q . k,q . (k + 1)]
then  k <= n + 1 by NAT_1:11;
then  k in H1(n + 1) ;
then A56: q . k = p . k by A48, A55;
 k + 1 in H1(n + 1) by A55;
then  q . (k + 1) = z by A48, A55;
hence  S1[k,q . k,q . (k + 1)] by A40, A55, A56; ::_thesis: verum
end;
hence  S1[k,q . k,q . (k + 1)] by A50; ::_thesis: verum
end;
A57: S2[ 0 ]
proof
set s = H1( 0 ) --> (the_rank_of F1());
take  H1( 0 ) --> (the_rank_of F1()) ; ::_thesis: ( dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) & (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Element of NAT st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) )
thus  dom (H1( 0 ) --> (the_rank_of F1())) = H1( 0 ) by FUNCOP_1:13; ::_thesis: ( (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() & ( for k being Element of NAT st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ) )
 0 in H1( 0 ) ;
hence  (H1( 0 ) --> (the_rank_of F1())) . 0 = the_rank_of F1() by FUNCOP_1:7; ::_thesis: for k being Element of NAT st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)]
thus  for k being Element of NAT st k < 0 holds
S1[k,(H1( 0 ) --> (the_rank_of F1())) . k,(H1( 0 ) --> (the_rank_of F1())) . (k + 1)] ; ::_thesis: verum
end;
thus  for n being Element of NAT holds S2[n] from NAT_1:sch_1(A57, A37); ::_thesis: verum
end;
 ex f being Function st
( dom f = NAT & ( for n being Element of NAT ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )
proof
defpred S2[ set , set ] means  for n being Element of NAT st n = $1 holds
ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & $2 = p . n );
A58: for x being set st x in NAT holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S2[x,y] )
assume  x in NAT ; ::_thesis: ex y being set st S2[x,y]
then reconsider n = x as Element of NAT ;
consider p being Function such that
A59: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) ) by A36;
take  p . n ; ::_thesis: S2[x,p . n]
let k be Element of NAT ; ::_thesis: ( k = x implies ex p being Function st
( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) )
assume A60: k = x ; ::_thesis: ex p being Function st
( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k )
take  p ; ::_thesis: ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k )
thus  ( dom p = H1(k) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < k holds
S1[k,p . k,p . (k + 1)] ) & p . n = p . k ) by A59, A60; ::_thesis: verum
end;
consider f being Function such that
A61: ( dom f = NAT & ( for x being set st x in NAT holds
S2[x,f . x] ) ) from CLASSES1:sch_1(A58);
take  f ; ::_thesis: ( dom f = NAT & ( for n being Element of NAT ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ) )
thus  dom f = NAT by A61; ::_thesis: for n being Element of NAT ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
let n be Element of NAT ; ::_thesis: ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
consider p being Function such that
A62: ( dom p = H1(n) & p . 0 = the_rank_of F1() ) and
A63: for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] and
A64: f . n = p . n by A61;
take  p ; ::_thesis: ( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
thus  ( dom p = H1(n) & p . 0 = the_rank_of F1() ) by A62; ::_thesis: ( ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n )
thus  for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] by A63; ::_thesis: f . n = p . n
thus  f . n = p . n by A64; ::_thesis: verum
end;
then consider f being Function such that
A65: dom f = NAT and
A66: for n being Element of NAT ex p being Function st
( dom p = H1(n) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < n holds
S1[k,p . k,p . (k + 1)] ) & f . n = p . n ) ;
take  f ; ::_thesis: ( dom f = NAT & f . 0 = the_rank_of F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) )
thus  dom f = NAT by A65; ::_thesis: ( f . 0 = the_rank_of F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) )
 ex p being Function st
( dom p = H1( 0 ) & p . 0 = the_rank_of F1() & ( for k being Element of NAT st k < 0 holds
S1[k,p . k,p . (k + 1)] ) & f . 0 = p . 0 ) by A66;
hence  f . 0 = the_rank_of F1() ; ::_thesis: for n being Element of NAT holds S1[n,f . n,f . (n + 1)]
let d be Element of NAT ; ::_thesis: S1[d,f . d,f . (d + 1)]
consider p being Function such that
A67: dom p = H1(d + 1) and
A68: p . 0 = the_rank_of F1() and
A69: for k being Element of NAT st k < d + 1 holds
S1[k,p . k,p . (k + 1)] and
A70: f . (d + 1) = p . (d + 1) by A66;
consider q being Function such that
A71: dom q = H1(d) and
A72: q . 0 = the_rank_of F1() and
A73: for k being Element of NAT st k < d holds
S1[k,q . k,q . (k + 1)] and
A74: f . d = q . d by A66;
 ( dom p = H1(d + 1) & dom q = H1(d) & p . 0 = q . 0 & ( for k being Element of NAT st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )
proof
thus  dom p = H1(d + 1) by A67; ::_thesis: ( dom q = H1(d) & p . 0 = q . 0 & ( for k being Element of NAT st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )
thus  dom q = H1(d) by A71; ::_thesis: ( p . 0 = q . 0 & ( for k being Element of NAT st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) ) )
thus  p . 0 = q . 0 by A68, A72; ::_thesis: for k being Element of NAT st k < d holds
( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] )
let k be Element of NAT ; ::_thesis: ( k < d implies ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] ) )
assume A75: k < d ; ::_thesis: ( S1[k,q . k,q . (k + 1)] & S1[k,p . k,p . (k + 1)] )
hence  S1[k,q . k,q . (k + 1)] by A73; ::_thesis: S1[k,p . k,p . (k + 1)]
 d <= d + 1 by NAT_1:11;
then  k < d + 1 by A75, XXREAL_0:2;
hence  S1[k,p . k,p . (k + 1)] by A69; ::_thesis: verum
end;
then  p . d = q . d by A28;
hence  S1[d,f . d,f . (d + 1)] by A69, A70, A74, XREAL_1:29; ::_thesis: verum
end;
then consider g being Function such that
A76: dom g = NAT and
A77: g . 0 = the_rank_of F1() and
A78: for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ;
defpred S2[ set , set ] means  ex i being Element of NAT st
( i = $1 `2 & P1[$1 `2 ,$1 `1 ,$2 `1 ] & $2 `2 = i + 1 & ( for y being set holds
( not P1[$1 `2 ,$1 `1 ,y] or not the_rank_of y in the_rank_of ($2 `1) ) ) );
A79: ( [F1(),0] `1 = F1() & [F1(),0] `2 = 0 ) ;
set beta = sup (rng g);
A80: for x being set st x in [:(Rank (sup (rng g))),NAT:] holds
ex u being set st S2[x,u]
proof
let x be set ; ::_thesis: ( x in [:(Rank (sup (rng g))),NAT:] implies ex u being set st S2[x,u] )
defpred S3[ Ordinal] means  ex y being set st
( y c= Rank $1 & P1[x `2 ,x `1 ,y] );
assume  x in [:(Rank (sup (rng g))),NAT:] ; ::_thesis: ex u being set st S2[x,u]
then consider a, b being set  such that
A81: a in Rank (sup (rng g)) and
A82: b in NAT and
A83: x = [a,b] by ZFMISC_1:def_2;
reconsider b = b as Element of NAT by A82;
A84: ( x `2 = b & x `1 = a ) by A83, MCART_1:7;
 the_rank_of a in sup (rng g) by A81, CLASSES1:66;
then consider alfa being Ordinal such that
A85: alfa in rng g and
A86: the_rank_of a c= alfa by ORDINAL2:21;
consider k being set  such that
A87: k in dom g and
A88: alfa = g . k by A85, FUNCT_1:def_3;
reconsider k = k as Element of NAT by A76, A87;
A89: S1[k,alfa,g . (k + 1)] by A78, A88;
then reconsider O2 = g . (k + 1) as Ordinal ;
 a c= Rank alfa by A86, CLASSES1:65;
then  a c= Rank (the_rank_of alfa) by CLASSES1:73;
then  ex y being set st
( y c= Rank O2 & P1[x `2 ,x `1 ,y] ) by A89, A84;
then A90: ex O being Ordinal st S3[O] ;
consider O being Ordinal such that
A91: S3[O] and
A92: for O9 being Ordinal st S3[O9] holds
O c= O9 from ORDINAL1:sch_1(A90);
consider Y being set  such that
A93: Y c= Rank O and
A94: P1[b,a,Y] by A84, A91;
A95: the_rank_of Y c= O by A93, CLASSES1:65;
take u = [Y,(b + 1)]; ::_thesis: S2[x,u]
take i = b; ::_thesis: ( i = x `2 & P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )
thus  i = x `2 by A83, MCART_1:7; ::_thesis: ( P1[x `2 ,x `1 ,u `1 ] & u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )
thus  P1[x `2 ,x `1 ,u `1 ] by A84, A94, MCART_1:7; ::_thesis: ( u `2 = i + 1 & ( for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) ) ) )
thus  u `2 = i + 1 by MCART_1:7; ::_thesis: for y being set holds
( not P1[x `2 ,x `1 ,y] or not the_rank_of y in the_rank_of (u `1) )
given y being set  such that A96: P1[x `2 ,x `1 ,y] and
A97: the_rank_of y in the_rank_of (u `1) ; ::_thesis: contradiction
A98: y c= Rank (the_rank_of y) by CLASSES1:def_8;
 the_rank_of y in the_rank_of Y by A97, MCART_1:7;
hence  contradiction by A92, A96, A95, A98, ORDINAL1:5; ::_thesis: verum
end;
consider F being Function such that
 dom F = [:(Rank (sup (rng g))),NAT:] and
A99: for x being set st x in [:(Rank (sup (rng g))),NAT:] holds
S2[x,F . x] from CLASSES1:sch_1(A80);
deffunc H1( Nat, set ) ->  set = (F . [$2,$1]) `1 ;
consider f being Function such that
A100: dom f = NAT and
A101: f . 0 = F1() and
A102: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_11();
defpred S3[ Element of NAT ] means  the_rank_of (f . $1) in sup (rng g);
 g . 0 in rng g by A76, FUNCT_1:def_3;
then A103: S3[ 0 ] by A77, A101, ORDINAL2:19;
A104: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A105: the_rank_of (f . n) in sup (rng g) ; ::_thesis: S3[n + 1]
then consider o1 being Ordinal such that
A106: o1 in rng g and
A107: the_rank_of (f . n) c= o1 by ORDINAL2:21;
 f . n in Rank (sup (rng g)) by A105, CLASSES1:66;
then A108: [(f . n),n] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87;
consider m being set  such that
A109: m in dom g and
A110: g . m = o1 by A106, FUNCT_1:def_3;
reconsider m = m as Element of NAT by A76, A109;
consider o2 being Ordinal such that
A111: o2 = g . (m + 1) and
A112: for X being set
for n being Element of NAT st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o2 & P1[n,X,Y] ) and
 for o being Ordinal st ( for X being set
for n being Element of NAT st X c= Rank (the_rank_of (g . m)) holds
ex Y being set st
( Y c= Rank o & P1[n,X,Y] ) ) holds
o2 c= o by A78;
 the_rank_of (f . n) c= the_rank_of (g . m) by A107, A110, CLASSES1:73;
then  f . n c= Rank (the_rank_of (g . m)) by CLASSES1:65;
then consider YY being set  such that
A113: YY c= Rank o2 and
A114: P1[n,f . n,YY] by A112;
A115: the_rank_of YY c= o2 by A113, CLASSES1:65;
 ( [(f . n),n] `1 = f . n & [(f . n),n] `2 = n ) ;
then  ex i being Element of NAT st
( i = n & P1[n,f . n,(F . [(f . n),n]) `1 ] & (F . [(f . n),n]) `2 = i + 1 & ( for y being set holds
( not P1[n,f . n,y] or not the_rank_of y in the_rank_of ((F . [(f . n),n]) `1) ) ) ) by A99, A108;
then A116: the_rank_of ((F . [(f . n),n]) `1) c= the_rank_of YY by A114, ORDINAL1:16;
 g . (m + 1) in rng g by A76, FUNCT_1:def_3;
then A117: o2 in sup (rng g) by A111, ORDINAL2:19;
 f . (n + 1) = (F . [(f . n),n]) `1 by A102;
hence  S3[n + 1] by A116, A115, A117, ORDINAL1:12, XBOOLE_1:1; ::_thesis: verum
end;
A118: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A103, A104);
defpred S4[ Element of NAT ] means P1[$1,f . $1,f . ($1 + 1)];
A119: for n being Element of NAT st S4[n] holds
S4[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S4[n] implies S4[n + 1] )
assume  P1[n,f . n,f . (n + 1)] ; ::_thesis: S4[n + 1]
 the_rank_of (f . (n + 1)) in sup (rng g) by A118;
then  f . (n + 1) in Rank (sup (rng g)) by CLASSES1:66;
then A120: [(f . (n + 1)),(n + 1)] in [:(Rank (sup (rng g))),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 Element of NAT st
( i = n + 1 & P1[n + 1,f . (n + 1),(F . [(f . (n + 1)),(n + 1)]) `1 ] & (F . [(f . (n + 1)),(n + 1)]) `2 = i + 1 & ( for y being set holds
( not P1[n + 1,f . (n + 1),y] or not the_rank_of y in the_rank_of ((F . [(f . (n + 1)),(n + 1)]) `1) ) ) ) by A99, A120;
hence  S4[n + 1] by A102; ::_thesis: verum
end;
take  f ; ::_thesis: ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
thus  dom f = NAT by A100; ::_thesis: ( f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
thus  f . 0 = F1() by A101; ::_thesis: for n being Element of NAT holds P1[n,f . n,f . (n + 1)]
 F1() in Rank (sup (rng g)) by A101, A103, CLASSES1:66;
then  [F1(),0] in [:(Rank (sup (rng g))),NAT:] by ZFMISC_1:87;
then  ex i being Element of NAT st
( i = [F1(),0] `2 & P1[ 0 ,F1(),(F . [F1(),0]) `1 ] & (F . [F1(),0]) `2 = i + 1 & ( for y being set holds
( not P1[ 0 ,F1(),y] or not the_rank_of y in the_rank_of ((F . [F1(),0]) `1) ) ) ) by A99, A79;
then A121: S4[ 0 ] by A101, A102;
thus  for n being Element of NAT holds S4[n] from NAT_1:sch_1(A121, A119); ::_thesis: verum
end;

scheme :: RECDEF_1:sch 2
RecExD{ F1() ->  non empty set , F2() ->  Element of F1(), P1[ set , set , set ] } :
 ex f being Function of NAT,F1() st
( f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
provided
A1: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof
defpred S1[ Element of NAT , set , set ] means P1[$1,$2,$3];
A2: for x being Element of NAT
for y being Element of F1() ex z being Element of F1() st S1[x,y,z] by A1;
consider f being Function of [:NAT,F1():],F1() such that
A3: for x being Element of NAT
for y being Element of F1() holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A2);
defpred S2[ FinSequence] means ( $1 . 1 = F2() & ( for n being Element of NAT st n + 2 <= len $1 holds
$1 . (n + 2) = f . [n,($1 . (n + 1))] ) );
consider X being set  such that
A4: for x being set holds
( x in X iff ex p being FinSequence st
( p in F1() * & S2[p] & x = p ) ) from FINSEQ_1:sch_4();
set Y = union X;
A5: for x being set st x in X holds
x in F1() *
proof
let x be set ; ::_thesis: ( x in X implies x in F1() * )
assume  x in X ; ::_thesis: x in F1() *
then  ex p being FinSequence st
( p in F1() * & p . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & x = p ) by A4;
hence  x in F1() * ; ::_thesis: verum
end;
A6: for p, q being FinSequence st p in X & q in X & len p <= len q holds
p c= q
proof
let p, q be FinSequence; ::_thesis: ( p in X & q in X & len p <= len q implies p c= q )
assume that
A7: p in X and
A8: q in X and
A9: len p <= len q ; ::_thesis: p c= q
A10: ex q9 being FinSequence st
( q9 in F1() * & q9 . 1 = F2() & ( for n being Element of NAT 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 F1() * & p9 . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p9 holds
p9 . (n + 2) = f . [n,(p9 . (n + 1))] ) & p = p9 ) by A4, A7;
A12: for n being Element of NAT st 1 <= n & n <= len p holds
p . n = q . n
proof
defpred S3[ Nat] means ( 1 <= $1 & $1 <= len p & p . $1 <> q . $1 );
assume  ex n being Element of NAT st S3[n] ; ::_thesis: contradiction
then A13: ex n being Nat st S3[n] ;
consider k being Nat such that
A14: ( S3[k] & ( for n being Nat st S3[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 ; ::_thesis: contradiction
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 = m as Element of NAT by ORDINAL1:def_12;
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  contradiction by A14; ::_thesis: verum
end;
hence  contradiction by A11, A10, A14; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_p_holds_
x_in_q
let x be set ; ::_thesis: ( x in p implies x in q )
assume  x in p ; ::_thesis: x in q
then consider n being 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, A22, A23, A25, A26;
hence  x in q by A27, FUNCT_1:1; ::_thesis: verum
end;
hence  p c= q by TARSKI:def_3; ::_thesis: verum
end;
 ex f being Function st f = union X
proof
defpred S3[ set , set ] means [$1,$2] in union X;
A28: for x, y, z being set st S3[x,y] & S3[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( S3[x,y] & S3[x,z] implies y = z )
assume that
A29: [x,y] in union X and
A30: [x,z] in union X ; ::_thesis: y = z
consider Z2 being set  such that
A31: [x,z] in Z2 and
A32: Z2 in X by A30, TARSKI:def_4;
 Z2 in F1() * by A5, A32;
then reconsider q = Z2 as FinSequence of F1() 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 F1() * by A5, A34;
then reconsider p = Z1 as FinSequence of F1() by FINSEQ_1:def_11;
A35: now__::_thesis:_(_len_q_<=_len_p_implies_y_=_z_)
assume  len q <= len p ; ::_thesis: y = z
then A36: q c= Z1 by A6, A34, A32;
 [x,y] in p by A33;
hence  y = z by A31, A36, FUNCT_1:def_1; ::_thesis: verum
end;
now__::_thesis:_(_len_p_<=_len_q_implies_y_=_z_)
assume  len p <= len q ; ::_thesis: y = z
then  p c= Z2 by A6, A34, A32;
then  [x,y] in q by A33;
hence  y = z by A31, FUNCT_1:def_1; ::_thesis: verum
end;
hence  y = z by A35; ::_thesis: verum
end;
consider h being Function such that
A37: for x, y being set holds
( [x,y] in h iff ( x in NAT & S3[x,y] ) ) from FUNCT_1:sch_1(A28);
take  h ; ::_thesis: h = union X
A38: for x, y being set holds
( [x,y] in h iff [x,y] in union X )
proof
let x, y be set ; ::_thesis: ( [x,y] in h iff [x,y] in union X )
thus  ( [x,y] in h implies [x,y] in union X ) by A37; ::_thesis: ( [x,y] in union X implies [x,y] in h )
thus  ( [x,y] in union X implies [x,y] in h ) ::_thesis: verum
proof
assume A39: [x,y] in union X ; ::_thesis: [x,y] in h
then consider Z being set  such that
A40: [x,y] in Z and
A41: Z in X by TARSKI:def_4;
 Z in F1() * by A5, A41;
then reconsider p = Z as FinSequence of F1() by FINSEQ_1:def_11;
 x in dom p by A40, XTUPLE_0:def_12;
hence  [x,y] in h by A37, A39; ::_thesis: verum
end;
end;
 for x being set holds
( x in h iff x in union X )
proof
let x be set ; ::_thesis: ( x in h iff x in union X )
thus  ( x in h implies x in union X ) ::_thesis: ( x in union X implies x in h )
proof
assume A42: x in h ; ::_thesis: x in union X
then  ex y, z being set st [y,z] = x by RELAT_1:def_1;
hence  x in union X by A38, A42; ::_thesis: verum
end;
assume A43: x in union X ; ::_thesis: x in h
then consider Z being set  such that
A44: x in Z and
A45: Z in X by TARSKI:def_4;
 Z in F1() * by A5, A45;
then reconsider p = Z as FinSequence of F1() by FINSEQ_1:def_11;
 x in p by A44;
then  ex y, z being set st [y,z] = x by RELAT_1:def_1;
hence  x in h by A38, A43; ::_thesis: verum
end;
hence  h = union X by TARSKI:1; ::_thesis: verum
end;
then consider g being Function such that
A46: g = union X ;
A47: for x being set st x in rng g holds
x in F1()
proof
let x be set ; ::_thesis: ( x in rng g implies x in F1() )
assume  x in rng g ; ::_thesis: x in F1()
then consider y being set  such that
A48: ( y in dom g & x = g . y ) by FUNCT_1:def_3;
 [y,x] in union X by A46, A48, FUNCT_1:1;
then consider Z being set  such that
A49: [y,x] in Z and
A50: Z in X by TARSKI:def_4;
 Z in F1() * by A5, A50;
then reconsider p = Z as FinSequence of F1() by FINSEQ_1:def_11;
 ( y in dom p & x = p . y ) by A49, FUNCT_1:1;
then A51: x in rng p by FUNCT_1:def_3;
 rng p c= F1() by FINSEQ_1:def_4;
hence  x in F1() by A51; ::_thesis: verum
end;
then  rng g c= F1() by TARSKI:def_3;
then reconsider h = g as Function of (dom g),F1() by FUNCT_2:2;
A52: for n being Element of NAT holds n + 1 in dom h
proof
defpred S3[ Element of NAT ] means $1 + 1 in dom h;
A53: for n being Element of NAT st n + 2 <= len <*F2()*> holds
<*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
proof
let n be Element of NAT ; ::_thesis: ( n + 2 <= len <*F2()*> implies <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] )
assume  n + 2 <= len <*F2()*> ; ::_thesis: <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
then  n + 2 <= 1 by FINSEQ_1:39;
then  n + (1 + 1) <= n + 1 by NAT_1:12;
hence  <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] by XREAL_1:6; ::_thesis: verum
end;
 ( <*F2()*> . 1 = F2() & <*F2()*> in F1() * ) by FINSEQ_1:def_8, FINSEQ_1:def_11;
then  <*F2()*> in X by A4, A53;
then A54: {[1,F2()]} in X by FINSEQ_1:37;
A55: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume  k + 1 in dom h ; ::_thesis: S3[k + 1]
then  [(k + 1),(h . (k + 1))] in union X by A46, FUNCT_1:1;
then consider Z being set  such that
A56: [(k + 1),(h . (k + 1))] in Z and
A57: Z in X by TARSKI:def_4;
 Z in F1() * by A5, A57;
then reconsider Z = Z as FinSequence of F1() by FINSEQ_1:def_11;
A58: ( k + 1 = len Z implies S3[k + 1] )
proof
set p = Z ^ <*(f . [k,(Z . (k + 1))])*>;
A59: 1 <= (k + 1) + 1 by NAT_1:12;
assume A60: k + 1 = len Z ; ::_thesis: S3[k + 1]
then  1 <= len Z by NAT_1:12;
then  1 in Seg (len Z) by FINSEQ_1:1;
then A61: 1 in dom Z by FINSEQ_1:def_3;
A62: for n being Element of NAT st n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) holds
(Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
proof
let n be Element of NAT ; ::_thesis: ( n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )
assume  n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) ; ::_thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
then A63: n + 2 <= (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22;
then A64: n + 2 <= (len Z) + 1 by FINSEQ_1:40;
A65: ( n + 2 <> (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )
proof
 (n + 1) + 1 <= (len Z) + 1 by A63, 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 A66: n + 1 in dom Z by FINSEQ_1:def_3;
A67: 1 <= n + (1 + 1) by NAT_1:12;
assume A68: n + 2 <> (len Z) + 1 ; ::_thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
then  n + 2 <= len Z by A64, NAT_1:8;
then  n + 2 in Seg (len Z) by A67, FINSEQ_1:1;
then A69: n + 2 in dom Z by FINSEQ_1:def_3;
 ex q being FinSequence st
( q in F1() * & q . 1 = F2() & ( for n being Element of NAT st n + 2 <= len q holds
q . (n + 2) = f . [n,(q . (n + 1))] ) & Z = q ) by A4, A57;
then  Z . (n + 2) = f . [n,(Z . (n + 1))] by A64, A68, NAT_1:8;
then  (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,(Z . (n + 1))] by A69, FINSEQ_1:def_7;
hence  (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A66, FINSEQ_1:def_7; ::_thesis: verum
end;
 ( n + 2 = (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )
proof
 (n + 1) + 1 <= (len Z) + 1 by A63, 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 A70: n + 1 in dom Z by FINSEQ_1:def_3;
assume A71: n + 2 = (len Z) + 1 ; ::_thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = <*(f . [k,(Z . (k + 1))])*> . ((n + 2) - ((n + 2) - 1)) by A63, FINSEQ_1:23
.= f . [n,(Z . (n + 1))] by A60, A71, FINSEQ_1:40 ;
hence  (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A70, FINSEQ_1:def_7; ::_thesis: verum
end;
hence  (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A65; ::_thesis: verum
end;
A72: Z ^ <*(f . [k,(Z . (k + 1))])*> in F1() *
proof
 1 <= k + 1 by NAT_1:12;
then  k + 1 in Seg (len Z) by A60, FINSEQ_1:1;
then  k + 1 in dom Z by FINSEQ_1:def_3;
then A73: Z . (k + 1) in rng Z by FUNCT_1:def_3;
 rng Z c= F1() by FINSEQ_1:def_4;
then reconsider z = Z . (k + 1) as Element of F1() by A73;
reconsider n = k as Element of NAT ;
 Z ^ <*(f . [k,(Z . (k + 1))])*> = Z ^ <*(f . [n,z])*> ;
hence  Z ^ <*(f . [k,(Z . (k + 1))])*> in F1() * by FINSEQ_1:def_11; ::_thesis: verum
end;
len (Z ^ <*(f . [k,(Z . (k + 1))])*>) = (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22
.= (k + 1) + 1 by A60, FINSEQ_1:39 ;
then  (k + 1) + 1 in Seg (len (Z ^ <*(f . [k,(Z . (k + 1))])*>)) by A59, FINSEQ_1:1;
then  (k + 1) + 1 in dom (Z ^ <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:def_3;
then A74: [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in Z ^ <*(f . [k,(Z . (k + 1))])*> by FUNCT_1:1;
 ex p being FinSequence st
( p in F1() * & p . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A57;
then  (Z ^ <*(f . [k,(Z . (k + 1))])*>) . 1 = F2() by A61, FINSEQ_1:def_7;
then  Z ^ <*(f . [k,(Z . (k + 1))])*> in X by A4, A72, A62;
then  [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in h by A46, A74, TARSKI:def_4;
hence  S3[k + 1] by FUNCT_1:1; ::_thesis: verum
end;
 ( k + 1 <> len Z implies S3[k + 1] )
proof
 k + 1 in dom Z by A56, FUNCT_1:1;
then  k + 1 in Seg (len Z) by FINSEQ_1:def_3;
then A75: k + 1 <= len Z by FINSEQ_1:1;
assume  k + 1 <> len Z ; ::_thesis: S3[k + 1]
then  k + 1 < len Z by A75, XXREAL_0:1;
then A76: (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 A76, 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 A46, A57, TARSKI:def_4;
hence  S3[k + 1] by FUNCT_1:1; ::_thesis: verum
end;
hence  S3[k + 1] by A58; ::_thesis: verum
end;
 [1,F2()] in {[1,F2()]} by TARSKI:def_1;
then  [1,F2()] in h by A46, A54, TARSKI:def_4;
then A77: S3[ 0 ] by FUNCT_1:1;
thus  for k being Element of NAT holds S3[k] from NAT_1:sch_1(A77, A55); ::_thesis: verum
end;
A78: for n being Element of NAT holds h . (n + 2) = f . [n,(h . (n + 1))]
proof
let n be Element of NAT ; ::_thesis: h . (n + 2) = f . [n,(h . (n + 1))]
 (n + 1) + 1 in dom h by A52;
then  [(n + 2),(h . (n + 2))] in h by FUNCT_1:def_2;
then consider Z being set  such that
A79: [(n + 2),(h . (n + 2))] in Z and
A80: Z in X by A46, TARSKI:def_4;
A81: ex p being FinSequence st
( p in F1() * & p . 1 = F2() & ( for n being Element of NAT st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A80;
 Z in F1() * by A5, A80;
then reconsider Z = Z as FinSequence of F1() by FINSEQ_1:def_11;
 n + 2 in dom Z by A79, FUNCT_1:1;
then  n + 2 in Seg (len Z) by FINSEQ_1:def_3;
then A82: 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 A82, 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 A83: [(n + 1),(Z . (n + 1))] in h by A46, A80, TARSKI:def_4;
thus h . (n + 2) = Z . (n + 2) by A79, FUNCT_1:1
.= f . [n,(Z . (n + 1))] by A81, A82
.= f . [n,(h . (n + 1))] by A83, FUNCT_1:1 ; ::_thesis: verum
end;
 ex g being Function of NAT,F1() st
for n being Element of NAT holds g . n = h . (n + 1)
proof
 ex g being Function st
( dom g = NAT & ( for n being Element of NAT holds g . n = h . (n + 1) ) )
proof
defpred S3[ set , set ] means  ex n being Element of NAT st
( n = $1 & $2 = h . (n + 1) );
A84: for x being set st x in NAT holds
ex y being set st S3[x,y]
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st S3[x,y] )
assume  x in NAT ; ::_thesis: ex y being set st S3[x,y]
then reconsider n = x as Element of NAT ;
take  h . (n + 1) ; ::_thesis: S3[x,h . (n + 1)]
take  n ; ::_thesis: ( n = x & h . (n + 1) = h . (n + 1) )
thus  ( n = x & h . (n + 1) = h . (n + 1) ) ; ::_thesis: verum
end;
consider g being Function such that
A85: ( dom g = NAT & ( for x being set st x in NAT holds
S3[x,g . x] ) ) from CLASSES1:sch_1(A84);
take  g ; ::_thesis: ( dom g = NAT & ( for n being Element of NAT holds g . n = h . (n + 1) ) )
thus  dom g = NAT by A85; ::_thesis: for n being Element of NAT holds g . n = h . (n + 1)
thus  for n being Element of NAT holds g . n = h . (n + 1) ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: g . n = h . (n + 1)
 ex m being Element of NAT st
( m = n & g . n = h . (m + 1) ) by A85;
hence  g . n = h . (n + 1) ; ::_thesis: verum
end;
end;
then consider g being Function such that
A86: dom g = NAT and
A87: for n being Element of NAT holds g . n = h . (n + 1) ;
 rng g c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in F1() )
assume  x in rng g ; ::_thesis: x in F1()
then consider y being set  such that
A88: y in dom g and
A89: x = g . y by FUNCT_1:def_3;
reconsider k = y as Element of NAT by A86, A88;
 k + 1 in dom h by A52;
then A90: h . (k + 1) in rng h by FUNCT_1:def_3;
 x = h . (k + 1) by A87, A89;
hence  x in F1() by A47, A90; ::_thesis: verum
end;
then reconsider g = g as Function of NAT,F1() by A86, FUNCT_2:2;
take  g ; ::_thesis: for n being Element of NAT holds g . n = h . (n + 1)
thus  for n being Element of NAT holds g . n = h . (n + 1) by A87; ::_thesis: verum
end;
then consider g being Function of NAT,F1() such that
A91: for n being Element of NAT holds g . n = h . (n + 1) ;
A92: for n being Element of NAT st n + 2 <= len <*F2()*> holds
<*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
proof
let n be Element of NAT ; ::_thesis: ( n + 2 <= len <*F2()*> implies <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] )
assume  n + 2 <= len <*F2()*> ; ::_thesis: <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
then  (n + 1) + 1 <= 0 + 1 by FINSEQ_1:39;
then  n + 1 <= 0 by XREAL_1:6;
then  n + 1 <= 0 + n ;
hence  <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] by XREAL_1:6; ::_thesis: verum
end;
 ( <*F2()*> in F1() * & <*F2()*> . 1 = F2() ) by FINSEQ_1:def_8, FINSEQ_1:def_11;
then  <*F2()*> in X by A4, A92;
then A93: {[1,F2()]} in X by FINSEQ_1:37;
take  g ; ::_thesis: ( g . 0 = F2() & ( for n being Element of NAT holds P1[n,g . n,g . (n + 1)] ) )
 [1,F2()] in {[1,F2()]} by TARSKI:def_1;
then  [1,F2()] in h by A46, A93, TARSKI:def_4;
then F2() = h . (0 + 1) by FUNCT_1:1
.= g . 0 by A91 ;
hence  g . 0 = F2() ; ::_thesis: for n being Element of NAT holds P1[n,g . n,g . (n + 1)]
let n be Element of NAT ; ::_thesis: P1[n,g . n,g . (n + 1)]
A94: h . (n + (1 + 1)) = f . (n,(h . (n + 1))) by A78;
 P1[n,g . n,f . (n,(g . n))] by A3;
then  P1[n,g . n,h . ((n + 1) + 1)] by A91, A94;
hence  P1[n,g . n,g . (n + 1)] by A91; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 3
FinRecEx{ F1() ->  set , F2() ->  Nat, P1[ set , set , set ] } :
 ex p being FinSequence st
( len p = F2() & ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)] ) )
provided
A1: for n being Element of NAT st 1 <= n & n < F2() holds
for x being set ex y being set st P1[n,x,y]
proof
defpred S1[ Element of NAT , set , set ] means ( ( $1 < F2() - 1 implies P1[$1 + 1,$2,$3] ) & ( not $1 < F2() - 1 implies $3 = 0 ) );
A2: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; ::_thesis: ex y being set st S1[n,x,y]
 ( n < F2() - 1 implies ex y being set st S1[n,x,y] )
proof
assume A3: n < F2() - 1 ; ::_thesis: ex y being set st S1[n,x,y]
then  n + 1 < F2() by XREAL_1:20;
then consider y being set  such that
A4: P1[n + 1,x,y] by A1, NAT_1:11;
take  y ; ::_thesis: S1[n,x,y]
thus  ( n < F2() - 1 implies P1[n + 1,x,y] ) by A4; ::_thesis: ( not n < F2() - 1 implies y = 0 )
thus  ( not n < F2() - 1 implies y = 0 ) by A3; ::_thesis: verum
end;
hence  ex y being set st S1[n,x,y] ; ::_thesis: verum
end;
consider f being Function such that
A5: ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_1(A2);
defpred S2[ set , set ] means  for r being Real st r = $1 holds
$2 = f . (r - 1);
A6: for x being set st x in REAL holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in REAL implies ex y being set st S2[x,y] )
assume  x in REAL ; ::_thesis: ex y being set st S2[x,y]
then reconsider r = x as Real ;
take  f . (r - 1) ; ::_thesis: S2[x,f . (r - 1)]
thus  S2[x,f . (r - 1)] ; ::_thesis: verum
end;
consider g being Function such that
A7: ( dom g = REAL & ( for x being set st x in REAL holds
S2[x,g . x] ) ) from CLASSES1:sch_1(A6);
A8: dom (g | (Seg F2())) = Seg F2() by A7, RELAT_1:62, XBOOLE_1:1;
then reconsider p = g | (Seg F2()) as FinSequence by FINSEQ_1:def_2;
take  p ; ::_thesis: ( len p = F2() & ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)] ) )
 F2() in NAT by ORDINAL1:def_12;
hence  len p = F2() by A8, FINSEQ_1:def_3; ::_thesis: ( ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)] ) )
 ( not F2() <> 0 or p . 1 = F1() or F2() = 0 )
proof
assume  F2() <> 0 ; ::_thesis: ( p . 1 = F1() or F2() = 0 )
then consider k being Nat such that
A9: F2() = k + 1 by NAT_1:6;
 0 + 1 <= k + 1 by XREAL_1:7;
then  1 in Seg F2() by A9, FINSEQ_1:1;
then p . 1 = g . 1 by FUNCT_1:49
.= f . (1 - 1) by A7
.= F1() by A5 ;
hence  ( p . 1 = F1() or F2() = 0 ) ; ::_thesis: verum
end;
hence  ( p . 1 = F1() or F2() = 0 ) ; ::_thesis: for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)]
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < F2() implies P1[n,p . n,p . (n + 1)] )
assume that
A10: 1 <= n and
A11: n < F2() ; ::_thesis: P1[n,p . n,p . (n + 1)]
 0 <> n by A10;
then consider k being Nat such that
A12: n = k + 1 by NAT_1:6;
A13: for n being Element of NAT st n < F2() holds
p . (n + 1) = f . n
proof
let n be Element of NAT ; ::_thesis: ( n < F2() implies p . (n + 1) = f . n )
assume  n < F2() ; ::_thesis: p . (n + 1) = f . n
then  ( 1 <= n + 1 & n + 1 <= F2() ) by NAT_1:11, NAT_1:13;
then A14: n + 1 in Seg F2() by FINSEQ_1:1;
g . (n + 1) = f . ((n + 1) - 1) by A7
.= f . n ;
hence  p . (n + 1) = f . n by A14, FUNCT_1:49; ::_thesis: verum
end;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 k <= k + 1 by NAT_1:11;
then A15: k < F2() by A11, A12, XXREAL_0:2;
 k < F2() - 1 by A11, A12, XREAL_1:20;
then  P1[k + 1,f . k,f . (k + 1)] by A5;
then  P1[k + 1,f . k,p . ((k + 1) + 1)] by A13, A11, A12;
hence  P1[n,p . n,p . (n + 1)] by A13, A12, A15; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 4
FinRecExD{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Nat, P1[ set , set , set ] } :
 ex p being FinSequence of F1() st
( len p = F3() & ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)] ) )
provided
A1: for n being Element of NAT st 1 <= n & n < F3() holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof
set 00 = the Element of F1();
defpred S1[ Element of NAT , set , set ] means ( ( $1 < F3() - 1 implies P1[$1 + 1,$2,$3] ) & ( not $1 < F3() - 1 implies $3 = the Element of F1() ) );
A2: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
let x be Element of F1(); ::_thesis: ex y being Element of F1() st S1[n,x,y]
 ( n < F3() - 1 implies ex y being Element of F1() st S1[n,x,y] )
proof
assume A3: n < F3() - 1 ; ::_thesis: ex y being Element of F1() st S1[n,x,y]
then  n + 1 < F3() by XREAL_1:20;
then consider y being Element of F1() such that
A4: P1[n + 1,x,y] by A1, NAT_1:11;
take  y ; ::_thesis: S1[n,x,y]
thus  ( n < F3() - 1 implies P1[n + 1,x,y] ) by A4; ::_thesis: ( not n < F3() - 1 implies y = the Element of F1() )
thus  ( not n < F3() - 1 implies y = the Element of F1() ) by A3; ::_thesis: verum
end;
hence  ex y being Element of F1() st S1[n,x,y] ; ::_thesis: verum
end;
consider f being Function of NAT,F1() such that
A5: ( f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A2);
defpred S2[ set , set ] means  for r being Real st r = $1 holds
$2 = f . (r - 1);
A6: for x being set st x in REAL holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in REAL implies ex y being set st S2[x,y] )
assume  x in REAL ; ::_thesis: ex y being set st S2[x,y]
then reconsider r = x as Real ;
take  f . (r - 1) ; ::_thesis: S2[x,f . (r - 1)]
thus  S2[x,f . (r - 1)] ; ::_thesis: verum
end;
consider g being Function such that
A7: ( dom g = REAL & ( for x being set st x in REAL holds
S2[x,g . x] ) ) from CLASSES1:sch_1(A6);
A8: dom (g | (Seg F3())) = Seg F3() by A7, RELAT_1:62, XBOOLE_1:1;
then reconsider p = g | (Seg F3()) as FinSequence by FINSEQ_1:def_2;
 rng p c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in F1() )
assume  x in rng p ; ::_thesis: x in F1()
then consider y being set  such that
A9: y in dom p and
A10: x = p . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A9;
A11: f . (y - 1) in F1()
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 = k as Element of NAT by ORDINAL1:def_12;
 f . k in F1() ;
hence  f . (y - 1) in F1() by A12; ::_thesis: verum
end;
 p . y = g . y by A9, FUNCT_1:47;
hence  x in F1() by A7, A10, A11; ::_thesis: verum
end;
then reconsider p = p as FinSequence of F1() by FINSEQ_1:def_4;
take  p ; ::_thesis: ( len p = F3() & ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)] ) )
 F3() in NAT by ORDINAL1:def_12;
hence  len p = F3() by A8, FINSEQ_1:def_3; ::_thesis: ( ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)] ) )
 ( not F3() <> 0 or p . 1 = F2() or F3() = 0 )
proof
assume  F3() <> 0 ; ::_thesis: ( p . 1 = F2() or F3() = 0 )
then consider k being Nat such that
A13: F3() = k + 1 by NAT_1:6;
 0 + 1 <= k + 1 by XREAL_1:7;
then  1 in Seg F3() by A13, FINSEQ_1:1;
then p . 1 = g . 1 by FUNCT_1:49
.= f . (1 - 1) by A7
.= F2() by A5 ;
hence  ( p . 1 = F2() or F3() = 0 ) ; ::_thesis: verum
end;
hence  ( p . 1 = F2() or F3() = 0 ) ; ::_thesis: for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)]
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < F3() implies P1[n,p . n,p . (n + 1)] )
assume that
A14: 1 <= n and
A15: n < F3() ; ::_thesis: P1[n,p . n,p . (n + 1)]
 0 <> n by A14;
then consider k being Nat such that
A16: n = k + 1 by NAT_1:6;
A17: for n being Element of NAT st n < F3() holds
p . (n + 1) = f . n
proof
let n be Element of NAT ; ::_thesis: ( n < F3() implies p . (n + 1) = f . n )
assume  n < F3() ; ::_thesis: p . (n + 1) = f . n
then  ( 1 <= n + 1 & n + 1 <= F3() ) by NAT_1:11, NAT_1:13;
then A18: n + 1 in Seg F3() by FINSEQ_1:1;
g . (n + 1) = f . ((n + 1) - 1) by A7
.= f . n ;
hence  p . (n + 1) = f . n by A18, FUNCT_1:49; ::_thesis: verum
end;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 k <= k + 1 by NAT_1:11;
then A19: k < F3() by A15, A16, XXREAL_0:2;
 k < F3() - 1 by A15, A16, XREAL_1:20;
then  P1[k + 1,f . k,f . (k + 1)] by A5;
then  P1[k + 1,f . k,p . ((k + 1) + 1)] by A17, A15, A16;
hence  P1[n,p . n,p . (n + 1)] by A17, A16, A19; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 5
SeqBinOpEx{ F1() ->  FinSequence, P1[ set , set , set ] } :
 ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
provided
A1: for k being Element of NAT
for x being set st 1 <= k & k < len F1() holds
ex y being set st P1[F1() . (k + 1),x,y]
proof
defpred S1[ Element of NAT , set , set ] means P1[F1() . ($1 + 1),$2,$3];
A2: for k being Element of NAT st 1 <= k & k < len F1() holds
for x being set ex y being set st S1[k,x,y] by A1;
consider p being FinSequence such that
A3: ( len p = len F1() & ( p . 1 = F1() . 1 or len F1() = 0 ) & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[k,p . k,p . (k + 1)] ) ) from RECDEF_1:sch_3(A2);
A4: ( len F1() <> 0 implies ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) )
proof
assume A5: len F1() <> 0 ; ::_thesis: ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
take  p . (len p) ; ::_thesis: ex p being FinSequence st
( p . (len p) = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
take  p ; ::_thesis: ( p . (len p) = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
thus  ( p . (len p) = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) by A3, A5; ::_thesis: for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)]
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < len F1() implies P1[F1() . (k + 1),p . k,p . (k + 1)] )
assume  ( 1 <= k & k < len F1() ) ; ::_thesis: P1[F1() . (k + 1),p . k,p . (k + 1)]
hence  P1[F1() . (k + 1),p . k,p . (k + 1)] by A3; ::_thesis: verum
end;
 ( len F1() = 0 implies ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) )
proof
assume A6: len F1() = 0 ; ::_thesis: ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
take  F1() . 0 ; ::_thesis: ex p being FinSequence st
( F1() . 0 = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
take  F1() ; ::_thesis: ( F1() . 0 = F1() . (len F1()) & len F1() = len F1() & F1() . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),F1() . k,F1() . (k + 1)] ) )
thus  ( F1() . 0 = F1() . (len F1()) & len F1() = len F1() & F1() . 1 = F1() . 1 ) by A6; ::_thesis: for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),F1() . k,F1() . (k + 1)]
thus  for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),F1() . k,F1() . (k + 1)] by A6; ::_thesis: verum
end;
hence  ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) by A4; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 6
LambdaSeqBinOpEx{ F1() ->  FinSequence, F2( set , set ) ->  set } :
 ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
proof
defpred S1[ set , set , set ] means $3 = F2($1,$2);
A1: for k being Element of NAT
for x being set st 1 <= k & k < len F1() holds
ex y being set st S1[F1() . (k + 1),x,y] ;
consider x being set  such that
A2: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[F1() . (k + 1),p . k,p . (k + 1)] ) ) from RECDEF_1:sch_5(A1);
take  x ; ::_thesis: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
consider p being FinSequence such that
A3: ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) and
A4: for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) by A2;
take  p ; ::_thesis: ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
thus  ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 ) by A3; ::_thesis: for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k))
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < len F1() implies p . (k + 1) = F2((F1() . (k + 1)),(p . k)) )
assume  ( 1 <= k & k < len F1() ) ; ::_thesis: p . (k + 1) = F2((F1() . (k + 1)),(p . k))
hence  p . (k + 1) = F2((F1() . (k + 1)),(p . k)) by A4; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 7
FinRecUn{ F1() ->  set , F2() ->  Nat, F3() ->  FinSequence, F4() ->  FinSequence, P1[ set , set , set ] } :
 F3() = F4()
provided
A1: for n being Element of NAT st 1 <= n & n < F2() holds
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 and
A2: ( len F3() = F2() & ( F3() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,F3() . n,F3() . (n + 1)] ) ) and
A3: ( len F4() = F2() & ( F4() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds
P1[n,F4() . n,F4() . (n + 1)] ) )
proof
defpred S1[ Nat] means ( 1 <= $1 & $1 <= F2() & F3() . $1 <> F4() . $1 );
assume A4: F3() <> F4() ; ::_thesis: contradiction
dom F3() = Seg (len F4()) by A2, A3, FINSEQ_1:def_3
.= dom F4() by FINSEQ_1:def_3 ;
then consider x being set  such that
A5: x in dom F3() and
A6: F3() . x <> F4() . x by A4, FUNCT_1:2;
A7: x in Seg (len F3()) by A5, FINSEQ_1:def_3;
reconsider x = x as Element of NAT by A5;
A8: 1 <= x by A7, FINSEQ_1:1;
 x <= F2() by A2, A7, FINSEQ_1:1;
then A9: ex n being Nat st S1[n] by A6, A8;
consider n being Nat such that
A10: ( S1[n] & ( for k being Nat st S1[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 = k as Element of NAT by ORDINAL1:def_12;
 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 < F2() by A10, XXREAL_0:2;
 n > k by A11, NAT_1:13;
then  F3() . k = F4() . k by A10, A12, A13;
then A14: P1[k,F3() . k,F4() . (k + 1)] by A3, A12, A13;
 P1[k,F3() . k,F3() . (k + 1)] by A2, A12, A13;
hence  contradiction by A1, A10, A11, A12, A13, A14; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 8
FinRecUnD{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Nat, F4() ->  FinSequence of F1(), F5() ->  FinSequence of F1(), P1[ set , set , set ] } :
 F4() = F5()
provided
A1: for n being Element of NAT st 1 <= n & n < F3() holds
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 and
A2: ( len F4() = F3() & ( F4() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,F4() . n,F4() . (n + 1)] ) ) and
A3: ( len F5() = F3() & ( F5() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds
P1[n,F5() . n,F5() . (n + 1)] ) )
proof
defpred S1[ Nat] means ( 1 <= $1 & $1 <= F3() & F4() . $1 <> F5() . $1 );
assume A4: F4() <> F5() ; ::_thesis: contradiction
dom F4() = Seg (len F5()) by A2, A3, FINSEQ_1:def_3
.= dom F5() by FINSEQ_1:def_3 ;
then consider x being set  such that
A5: x in dom F4() and
A6: F4() . x <> F5() . x by A4, FUNCT_1:2;
A7: x in Seg (len F4()) by A5, FINSEQ_1:def_3;
reconsider x = x as Element of NAT by A5;
A8: 1 <= x by A7, FINSEQ_1:1;
 x <= F3() by A2, A7, FINSEQ_1:1;
then A9: ex n being Nat st S1[n] by A6, A8;
consider n being Nat such that
A10: ( S1[n] & ( for k being Nat st S1[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 = k as Element of NAT by ORDINAL1:def_12;
reconsider Gk1 = F5() . (k + 1) as Element of F1() 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 < F3() by A10, XXREAL_0:2;
then reconsider Fk = F4() . k as Element of F1() by A2, A12, Lm1;
 n > k by A11, NAT_1:13;
then  F4() . k = F5() . k by A10, A12, A13;
then A14: P1[k,Fk,Gk1] by A3, A12, A13;
reconsider Fk1 = F4() . (k + 1) as Element of F1() by A2, A10, A11, Lm1;
 P1[k,Fk,Fk1] by A2, A12, A13;
hence  contradiction by A1, A10, A11, A12, A13, A14; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 9
SeqBinOpUn{ F1() ->  FinSequence, P1[ set , set , set ], F2() ->  set , F3() ->  set } :
 F2() = F3()
provided
A1: for k being Element of NAT
for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds
y1 = y2 and
A2: ex p being FinSequence st
( F2() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) and
A3: ex p being FinSequence st
( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
proof
defpred S1[ Element of NAT , set , set ] means P1[F1() . ($1 + 1),$2,$3];
A4: for k being Element of NAT st 1 <= k & k < len F1() holds
for x, y1, y2 being set st S1[k,x,y1] & S1[k,x,y2] holds
y1 = y2 by A1;
consider q being FinSequence such that
A5: F3() = q . (len q) and
A6: ( len q = len F1() & q . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[k,q . k,q . (k + 1)] ) ) by A3;
A7: ( len q = len F1() & ( q . 1 = F1() . 1 or len F1() = 0 ) & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[k,q . k,q . (k + 1)] ) ) by A6;
consider p being FinSequence such that
A8: F2() = p . (len p) and
A9: ( len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[k,p . k,p . (k + 1)] ) ) by A2;
A10: ( len p = len F1() & ( p . 1 = F1() . 1 or len F1() = 0 ) & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[k,p . k,p . (k + 1)] ) ) by A9;
 p = q from RECDEF_1:sch_7(A4, A10, A7);
hence  F2() = F3() by A8, A5; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 10
LambdaSeqBinOpUn{ F1() ->  FinSequence, F2( set , set ) ->  set , F3() ->  set , F4() ->  set } :
 F3() = F4()
provided
A1: ex p being FinSequence st
( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) and
A2: ex p being FinSequence st
( F4() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
proof
defpred S1[ set , set , set ] means $3 = F2($1,$2);
A3: ex p being FinSequence st
( F4() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[F1() . (k + 1),p . k,p . (k + 1)] ) ) by A2;
A4: for k being Element of NAT
for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & S1[z,x,y1] & S1[z,x,y2] holds
y1 = y2 ;
A5: ex p being FinSequence st
( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
S1[F1() . (k + 1),p . k,p . (k + 1)] ) ) by A1;
thus  F3() = F4() from RECDEF_1:sch_9(A4, A5, A3); ::_thesis: verum
end;

scheme :: RECDEF_1:sch 11
DefRec{ F1() ->  set , F2() ->  Nat, P1[ set , set , set ] } :
 ( ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )
provided
A1: for n being Element of NAT
for x being set ex y being set st P1[n,x,y] and
A2: for n being Element of NAT
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof
A3: for n being Element of NAT
for x being set ex y being set st P1[n,x,y] by A1;
consider f being Function such that
A4: ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_1(A3);
A5: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof
let n be Nat; ::_thesis: for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
 n in NAT by ORDINAL1:def_12;
hence  for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 by A2; ::_thesis: verum
end;
thus  ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) ::_thesis: for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2
proof
take  f . F2() ; ::_thesis: ex f being Function st
( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
take  f ; ::_thesis: ( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
thus  ( f . F2() = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) by A4; ::_thesis: verum
end;
let y1, y2 be set ; ::_thesis: ( ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) implies y1 = y2 )
given f1 being Function such that A6: y1 = f1 . F2() and
A7: dom f1 = NAT and
A8: f1 . 0 = F1() and
A9: for n being Element of NAT holds P1[n,f1 . n,f1 . (n + 1)] ; ::_thesis: ( for f being Function holds
( not y2 = f . F2() or not dom f = NAT or not f . 0 = F1() or ex n being Element of NAT st P1[n,f . n,f . (n + 1)] ) or y1 = y2 )
A10: for n being Nat holds P1[n,f1 . n,f1 . (n + 1)]
proof
let n be Nat; ::_thesis: P1[n,f1 . n,f1 . (n + 1)]
 n in NAT by ORDINAL1:def_12;
hence  P1[n,f1 . n,f1 . (n + 1)] by A9; ::_thesis: verum
end;
given f2 being Function such that A11: y2 = f2 . F2() and
A12: dom f2 = NAT and
A13: f2 . 0 = F1() and
A14: for n being Element of NAT holds P1[n,f2 . n,f2 . (n + 1)] ; ::_thesis: y1 = y2
A15: for n being Nat holds P1[n,f2 . n,f2 . (n + 1)]
proof
let n be Nat; ::_thesis: P1[n,f2 . n,f2 . (n + 1)]
 n in NAT by ORDINAL1:def_12;
hence  P1[n,f2 . n,f2 . (n + 1)] by A14; ::_thesis: verum
end;
 f1 = f2 from NAT_1:sch_13(A7, A8, A10, A12, A13, A15, A5);
hence  y1 = y2 by A6, A11; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 12
LambdaDefRec{ F1() ->  set , F2() ->  Nat, F3( set , set ) ->  set } :
 ( ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) holds
y1 = y2 ) )
proof
defpred S1[ set , set , set ] means  for z being set st z = $2 holds
$3 = F3($1,z);
A1: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; ::_thesis: ex y being set st S1[n,x,y]
take  F3(n,x) ; ::_thesis: S1[n,x,F3(n,x)]
let z be set ; ::_thesis: ( z = x implies F3(n,x) = F3(n,z) )
assume  z = x ; ::_thesis: F3(n,x) = F3(n,z)
hence  F3(n,x) = F3(n,z) ; ::_thesis: verum
end;
A2: for n being Element of NAT
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be Element of NAT ; ::_thesis: for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
let x, y1, y2 be set ; ::_thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that
A3: for z being set st z = x holds
y1 = F3(n,z) and
A4: for z being set st z = x holds
y2 = F3(n,z) ; ::_thesis: y1 = y2
thus y1 = F3(n,x) by A3
.= y2 by A4 ; ::_thesis: verum
end;
A5: ( ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) ) from RECDEF_1:sch_11(A1, A2);
then consider y being set , f being Function such that
A6: ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) ;
thus  ex y being set ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) ::_thesis: for y1, y2 being set st ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) holds
y1 = y2
proof
take  y ; ::_thesis: ex f being Function st
( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) )
take  f ; ::_thesis: ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) )
thus  ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) by A6; ::_thesis: verum
end;
let y1, y2 be set ; ::_thesis: ( ex f being Function st
( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st
( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) implies y1 = y2 )
given f1 being Function such that A7: ( y1 = f1 . F2() & dom f1 = NAT & f1 . 0 = F1() ) and
A8: for n being Element of NAT holds f1 . (n + 1) = F3(n,(f1 . n)) ; ::_thesis: ( for f being Function holds
( not y2 = f . F2() or not dom f = NAT or not f . 0 = F1() or ex n being Element of NAT st not f . (n + 1) = F3(n,(f . n)) ) or y1 = y2 )
A9: for n being Element of NAT holds S1[n,f1 . n,f1 . (n + 1)] by A8;
given f2 being Function such that A10: ( y2 = f2 . F2() & dom f2 = NAT & f2 . 0 = F1() ) and
A11: for n being Element of NAT holds f2 . (n + 1) = F3(n,(f2 . n)) ; ::_thesis: y1 = y2
 for n being Element of NAT holds S1[n,f2 . n,f2 . (n + 1)] by A11;
hence  y1 = y2 by A5, A7, A10, A9; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 13
DefRecD{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Nat, P1[ set , set , set ] } :
 ( ex y being Element of F1() ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )
provided
A1: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st P1[n,x,y] and
A2: for n being Element of NAT
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof
A3: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st P1[n,x,y] by A1;
consider f being Function of NAT,F1() such that
A4: ( f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A3);
A5: for n being Nat
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof
let n be Nat; ::_thesis: for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
 n in NAT by ORDINAL1:def_12;
hence  for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2 by A2; ::_thesis: verum
end;
thus  ex y being Element of F1() ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) ::_thesis: for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2
proof
reconsider n = F3() as Element of NAT by ORDINAL1:def_12;
take  f . n ; ::_thesis: ex f being Function of NAT,F1() st
( f . n = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
take  f ; ::_thesis: ( f . n = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) )
thus  ( f . n = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) by A4; ::_thesis: verum
end;
let y1, y2 be Element of F1(); ::_thesis: ( ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) implies y1 = y2 )
given f1 being Function of NAT,F1() such that A6: y1 = f1 . F3() and
A7: f1 . 0 = F2() and
A8: for n being Element of NAT holds P1[n,f1 . n,f1 . (n + 1)] ; ::_thesis: ( for f being Function of NAT,F1() holds
( not y2 = f . F3() or not f . 0 = F2() or ex n being Element of NAT st P1[n,f . n,f . (n + 1)] ) or y1 = y2 )
A9: f1 . 0 = F2() by A7;
A10: for n being Nat holds P1[n,f1 . n,f1 . (n + 1)]
proof
let n be Nat; ::_thesis: P1[n,f1 . n,f1 . (n + 1)]
 n in NAT by ORDINAL1:def_12;
hence  P1[n,f1 . n,f1 . (n + 1)] by A8; ::_thesis: verum
end;
given f2 being Function of NAT,F1() such that A11: y2 = f2 . F3() and
A12: f2 . 0 = F2() and
A13: for n being Element of NAT holds P1[n,f2 . n,f2 . (n + 1)] ; ::_thesis: y1 = y2
A14: for n being Nat holds P1[n,f2 . n,f2 . (n + 1)]
proof
let n be Nat; ::_thesis: P1[n,f2 . n,f2 . (n + 1)]
 n in NAT by ORDINAL1:def_12;
hence  P1[n,f2 . n,f2 . (n + 1)] by A13; ::_thesis: verum
end;
A15: f2 . 0 = F2() by A12;
 f1 = f2 from NAT_1:sch_14(A9, A10, A15, A14, A5);
hence  y1 = y2 by A6, A11; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 14
LambdaDefRecD{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Nat, F4( set , set ) ->  Element of F1() } :
 ( ex y being Element of F1() ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds
y1 = y2 ) )
proof
defpred S1[ set , set , set ] means  for z being Element of F1() st z = $2 holds
$3 = F4($1,z);
A1: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
let x be Element of F1(); ::_thesis: ex y being Element of F1() st S1[n,x,y]
take  F4(n,x) ; ::_thesis: S1[n,x,F4(n,x)]
let z be Element of F1(); ::_thesis: ( z = x implies F4(n,x) = F4(n,z) )
assume  z = x ; ::_thesis: F4(n,x) = F4(n,z)
hence  F4(n,x) = F4(n,z) ; ::_thesis: verum
end;
A2: for n being Element of NAT
for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
proof
let n be Element of NAT ; ::_thesis: for x, y1, y2 being Element of F1() st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2
let x, y1, y2 be Element of F1(); ::_thesis: ( S1[n,x,y1] & S1[n,x,y2] implies y1 = y2 )
assume that
A3: for z being Element of F1() st z = x holds
y1 = F4(n,z) and
A4: for z being Element of F1() st z = x holds
y2 = F4(n,z) ; ::_thesis: y1 = y2
thus y1 = F4(n,x) by A3
.= y2 by A4 ; ::_thesis: verum
end;
A5: ( ex y being Element of F1() ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) ) from RECDEF_1:sch_13(A1, A2);
then consider y being Element of F1(), f being Function of NAT,F1() such that
A6: ( y = f . F3() & f . 0 = F2() ) and
A7: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ;
thus  ex y being Element of F1() ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) ::_thesis: for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds
y1 = y2
proof
take  y ; ::_thesis: ex f being Function of NAT,F1() st
( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) )
take  f ; ::_thesis: ( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) )
thus  ( y = f . F3() & f . 0 = F2() ) by A6; ::_thesis: for n being Nat holds f . (n + 1) = F4(n,(f . n))
let n be Nat; ::_thesis: f . (n + 1) = F4(n,(f . n))
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 S1[n,f . n,f . (n + 1)] by A7;
hence  f . (n + 1) = F4(n,(f . n)) ; ::_thesis: verum
end;
let y1, y2 be Element of F1(); ::_thesis: ( ex f being Function of NAT,F1() st
( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st
( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) implies y1 = y2 )
given f being Function of NAT,F1() such that A8: ( y1 = f . F3() & f . 0 = F2() ) and
A9: for n being Nat holds f . (n + 1) = F4(n,(f . n)) ; ::_thesis: ( for f being Function of NAT,F1() holds
( not y2 = f . F3() or not f . 0 = F2() or ex n being Nat st not f . (n + 1) = F4(n,(f . n)) ) or y1 = y2 )
A10: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] by A9;
given f2 being Function of NAT,F1() such that A11: ( y2 = f2 . F3() & f2 . 0 = F2() ) and
A12: for n being Nat holds f2 . (n + 1) = F4(n,(f2 . n)) ; ::_thesis: y1 = y2
 for n being Element of NAT holds S1[n,f2 . n,f2 . (n + 1)] by A12;
hence  y1 = y2 by A5, A8, A11, A10; ::_thesis: verum
end;

scheme :: RECDEF_1:sch 15
SeqBinOpDef{ F1() ->  FinSequence, P1[ set , set , set ] } :
 ( ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ( for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) holds
x = y ) )
provided
A1: for k being Element of NAT
for y being set st 1 <= k & k < len F1() holds
ex z being set st P1[F1() . (k + 1),y,z] and
A2: for k being Element of NAT
for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds
y1 = y2
proof
A3: for k being Element of NAT
for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds
y1 = y2 by A2;
A4: for k being Element of NAT
for y being set st 1 <= k & k < len F1() holds
ex z being set st P1[F1() . (k + 1),y,z] by A1;
thus  ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) from RECDEF_1:sch_5(A4); ::_thesis: for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) holds
x = y
let x, y be set ; ::_thesis: ( ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) implies x = y )
assume A5: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ; ::_thesis: ( for p being FinSequence holds
( not y = p . (len p) or not len p = len F1() or not p . 1 = F1() . 1 or ex k being Element of NAT st
( 1 <= k & k < len F1() & P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) or x = y )
assume A6: ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ; ::_thesis: x = y
thus  x = y from RECDEF_1:sch_9(A3, A5, A6); ::_thesis: verum
end;

scheme :: RECDEF_1:sch 16
LambdaSeqBinOpDef{ F1() ->  FinSequence, F2( set , set ) ->  set } :
 ( ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ( for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) holds
x = y ) )
proof
thus  ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) from RECDEF_1:sch_6(); ::_thesis: for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) holds
x = y
let x, y be set ; ::_thesis: ( ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) implies x = y )
assume A1: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) ; ::_thesis: ( for p being FinSequence holds
( not y = p . (len p) or not len p = len F1() or not p . 1 = F1() . 1 or ex k being Element of NAT st
( 1 <= k & k < len F1() & not p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) or x = y )
assume A2: ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) ; ::_thesis: x = y
thus  x = y from RECDEF_1:sch_10(A1, A2); ::_thesis: verum
end;

scheme :: RECDEF_1:sch 17
SeqExD{ F1() ->  non empty set , F2() ->  Element of NAT , P1[ set , set ] } :
 ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,p /. k] ) )
provided
A1: for k being Element of NAT st k in Seg F2() holds
ex x being Element of F1() st P1[k,x]
proof
percases ( F2() = 0 or F2() <> 0 ) ;
supposeA2: F2() = 0 ; ::_thesis: ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,p /. k] ) )
take  <*> F1() ; ::_thesis: ( dom (<*> F1()) = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,(<*> F1()) /. k] ) )
thus  ( dom (<*> F1()) = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,(<*> F1()) /. k] ) ) by A2; ::_thesis: verum
end;
supposeA3: F2() <> 0 ; ::_thesis: ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,p /. k] ) )
now__::_thesis:_not_Seg_F2()_=_{}
assume A4: Seg F2() = {} ; ::_thesis: contradiction
now__::_thesis:_(_(_F2()_=_0_&_contradiction_)_or_(_F2()_<>_0_&_contradiction_)_)
percases ( F2() = 0 or F2() <> 0 ) ;
case F2() = 0 ; ::_thesis: contradiction
hence  contradiction by A3; ::_thesis: verum
end;
case F2() <> 0 ; ::_thesis: contradiction
hence  contradiction by A4; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
then reconsider M = Seg F2() as non empty set ;
A5: for x being Element of M ex y being Element of F1() st P1[x,y]
proof
let x be Element of M; ::_thesis: ex y being Element of F1() st P1[x,y]
 x in Seg F2() ;
hence  ex y being Element of F1() st P1[x,y] by A1; ::_thesis: verum
end;
consider f being Function of M,F1() such that
A6: for x being Element of M holds P1[x,f . x] from FUNCT_2:sch_3(A5);
 dom f = Seg F2() by FUNCT_2:def_1;
then reconsider q = f as FinSequence by FINSEQ_1:def_2;
now__::_thesis:_for_u_being_set_st_u_in_rng_q_holds_
u_in_F1()
let u be set ; ::_thesis: ( u in rng q implies u in F1() )
A7: rng q c= F1() by RELAT_1:def_19;
assume  u in rng q ; ::_thesis: u in F1()
hence  u in F1() by A7; ::_thesis: verum
end;
then  rng q c= F1() by TARSKI:def_3;
then reconsider q = q as FinSequence of F1() by FINSEQ_1:def_4;
take  q ; ::_thesis: ( dom q = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,q /. k] ) )
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_Seg_F2()_holds_
P1[k,q_/._k]
let k be Element of NAT ; ::_thesis: ( k in Seg F2() implies P1[k,q /. k] )
assume A8: k in Seg F2() ; ::_thesis: P1[k,q /. k]
then  k in dom q by FUNCT_2:def_1;
then  q . k = q /. k by PARTFUN1:def_6;
hence  P1[k,q /. k] by A6, A8; ::_thesis: verum
end;
hence  ( dom q = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds
P1[k,q /. k] ) ) by FUNCT_2:def_1; ::_thesis: verum
end;
end;
end;

scheme :: RECDEF_1:sch 18
FinRecExD2{ F1() ->  non empty set , F2() ->  Element of F1(), F3() ->  Element of NAT , P1[ set , set , set ] } :
 ex p being FinSequence of F1() st
( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)] ) )
provided
A1: for n being Element of NAT st 1 <= n & n <= F3() - 1 holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof
set 00 = the Element of F1();
defpred S1[ Element of NAT , set , set ] means ( ( 0 <= $1 & $1 <= F3() - 2 implies P1[$1 + 1,$2,$3] ) & ( ( not 0 <= $1 or not $1 <= F3() - 2 ) implies $3 = the Element of F1() ) );
A2: for n being Element of NAT
for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of F1() ex y being Element of F1() st S1[n,x,y]
let x be Element of F1(); ::_thesis: ex y being Element of F1() st S1[n,x,y]
 ( 0 <= n & n <= F3() - 2 implies ex y being Element of F1() st S1[n,x,y] )
proof
A3: 0 + 1 <= n + 1 by XREAL_1:6;
assume that
 0 <= n and
A4: n <= F3() - 2 ; ::_thesis: ex y being Element of F1() st S1[n,x,y]
 n + 1 <= (F3() - 2) + 1 by A4, XREAL_1:6;
then consider y being Element of F1() such that
A5: P1[n + 1,x,y] by A1, A3;
take  y ; ::_thesis: S1[n,x,y]
thus  ( 0 <= n & n <= F3() - 2 implies P1[n + 1,x,y] ) by A5; ::_thesis: ( ( not 0 <= n or not n <= F3() - 2 ) implies y = the Element of F1() )
thus  ( ( not 0 <= n or not n <= F3() - 2 ) implies y = the Element of F1() ) by A4; ::_thesis: verum
end;
hence  ex y being Element of F1() st S1[n,x,y] ; ::_thesis: verum
end;
consider f being Function of NAT,F1() such that
A6: ( f . 0 = F2() & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A2);
defpred S2[ set , set ] means  for r being Real st r = $1 holds
$2 = f . (r - 1);
A7: for x being set st x in REAL holds
ex y being set st S2[x,y]
proof
let x be set ; ::_thesis: ( x in REAL implies ex y being set st S2[x,y] )
assume  x in REAL ; ::_thesis: ex y being set st S2[x,y]
then reconsider r = x as Real ;
take  f . (r - 1) ; ::_thesis: S2[x,f . (r - 1)]
thus  S2[x,f . (r - 1)] ; ::_thesis: verum
end;
consider g being Function such that
A8: ( dom g = REAL & ( for x being set st x in REAL holds
S2[x,g . x] ) ) from CLASSES1:sch_1(A7);
A9: dom (g | (Seg F3())) = Seg F3() by A8, RELAT_1:62, XBOOLE_1:1;
then reconsider p = g | (Seg F3()) as FinSequence by FINSEQ_1:def_2;
now__::_thesis:_for_x_being_set_st_x_in_rng_p_holds_
x_in_F1()
let x be set ; ::_thesis: ( x in rng p implies x in F1() )
assume  x in rng p ; ::_thesis: x in F1()
then consider y being set  such that
A10: y in dom p and
A11: x = p . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A10;
A12: f . (y - 1) in F1()
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 = k as Element of NAT by ORDINAL1:def_12;
 f . k in F1() ;
hence  f . (y - 1) in F1() by A13; ::_thesis: verum
end;
 p . y = g . y by A10, FUNCT_1:47;
hence  x in F1() by A8, A11, A12; ::_thesis: verum
end;
then  rng p c= F1() by TARSKI:def_3;
then reconsider p = p as FinSequence of F1() by FINSEQ_1:def_4;
take  p ; ::_thesis: ( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)] ) )
thus  len p = F3() by A9, FINSEQ_1:def_3; ::_thesis: ( ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)] ) )
 ( F3() <> 0 implies p /. 1 = F2() )
proof
assume  F3() <> 0 ; ::_thesis: p /. 1 = F2()
then consider k being Nat such that
A14: F3() = k + 1 by NAT_1:6;
 0 + 1 <= k + 1 by XREAL_1:7;
then A15: 1 in Seg F3() by A14, FINSEQ_1:1;
then p /. 1 = p . 1 by A9, PARTFUN1:def_6
.= g . 1 by A15, FUNCT_1:49
.= f . (1 - 1) by A8
.= F2() by A6 ;
hence  p /. 1 = F2() ; ::_thesis: verum
end;
hence  ( p /. 1 = F2() or F3() = 0 ) ; ::_thesis: for n being Element of NAT st 1 <= n & n <= F3() - 1 holds
P1[n,p /. n,p /. (n + 1)]
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= F3() - 1 implies P1[n,p /. n,p /. (n + 1)] )
assume that
A16: 1 <= n and
A17: n <= F3() - 1 ; ::_thesis: P1[n,p /. n,p /. (n + 1)]
consider k being Nat such that
A18: n = k + 1 by A16, NAT_1:6;
A19: for n being Element of NAT st n <= F3() - 1 holds
p /. (n + 1) = f . n
proof
let n be Element of NAT ; ::_thesis: ( n <= F3() - 1 implies p /. (n + 1) = f . n )
assume  n <= F3() - 1 ; ::_thesis: p /. (n + 1) = f . n
then A20: n + 1 <= (F3() - 1) + 1 by XREAL_1:6;
A21: g . (n + 1) = f . ((n + 1) - 1) by A8
.= f . n ;
 1 <= n + 1 by NAT_1:11;
then A22: n + 1 in Seg F3() by A20, FINSEQ_1:1;
then  p /. (n + 1) = p . (n + 1) by A9, PARTFUN1:def_6;
hence  p /. (n + 1) = f . n by A22, A21, FUNCT_1:49; ::_thesis: verum
end;
A23: k <= k + 1 by NAT_1:11;
A24: k in NAT by ORDINAL1:def_12;
 k <= (F3() - 1) - 1 by A17, A18, XREAL_1:19;
then  P1[k + 1,f . k,f . (k + 1)] by A6, A24;
then  P1[k + 1,f . k,p /. ((k + 1) + 1)] by A19, A17, A18;
hence  P1[n,p /. n,p /. (n + 1)] by A19, A17, A18, A24, A23, XXREAL_0:2; ::_thesis: verum
end;