defpred S₁[ object , FinSequence-yielding FinSequence] means ex p being FinSequence st
( p = $1 & len p = len $2 & ( for i being Nat st i in dom p holds
p . i in dom ($2 . i) ) );
defpred S₂[ Nat] means for H being FinSequence-yielding FinSequence st len H = $1 holds
ex IT being finite FinSequence-membered set st
for x being object holds
( x in IT iff S₁[x,H] );
A1: S₂[ 0 ]

proof

let H be FinSequence-yielding FinSequence; :: thesis: ( len H = 0 implies ex IT being finite FinSequence-membered set st
for x being object holds
( x in IT iff S₁[x,H] ) )
assume A2: len H = 0 ; :: thesis: ex IT being finite FinSequence-membered set st
for x being object holds
( x in IT iff S₁[x,H] )
take IT = {{}}; :: thesis: for x being object holds
( x in IT iff S₁[x,H] )
let x be object ; :: thesis: ( x in IT iff S₁[x,H] )
thus ( x in IT implies S₁[x,H] ) :: thesis: ( S₁[x,H] implies x in IT )

proof

assume A3: x in IT ; :: thesis: S₁[x,H]
take p = {} ; :: thesis: ( p = x & len p = len H & ( for i being Nat st i in dom p holds
p . i in dom (H . i) ) )
thus ( p = x & len p = len H & ( for i being Nat st i in dom p holds
p . i in dom (H . i) ) ) by A2, A3; :: thesis: verum

end;

given p being FinSequence such that A4: ( p = x & len p = len H & ( for i being Nat st i in dom p holds
p . i in dom (H . i) ) ) ; :: thesis: x in IT
p = {} by A4, A2;
hence x in IT by A4, TARSKI:def 1; :: thesis: verum

end;

A5: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
set n1 = n + 1;
assume A6: S₂[n] ; :: thesis: S₂[n + 1]
let H be FinSequence-yielding FinSequence; :: thesis: ( len H = n + 1 implies ex IT being finite FinSequence-membered set st
for x being object holds
( x in IT iff S₁[x,H] ) )
assume A7: len H = n + 1 ; :: thesis: ex IT being finite FinSequence-membered set st
for x being object holds
( x in IT iff S₁[x,H] )
A8: ( 1 <= n + 1 & n < n + 1 ) by NAT_1:11, NAT_1:13;
reconsider Hn = H | n as FinSequence-yielding FinSequence ;
A9: len Hn = n by NAT_1:11, FINSEQ_1:59, A7;
then consider IT being finite FinSequence-membered set such that
A10: for x being object holds
( x in IT iff S₁[x,Hn] ) by A6;
set IT2 = { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } ;
A11: { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } is finite

proof

per cases ( IT is empty or dom (H . (n + 1)) is empty or ( not IT is empty & not dom (H . (n + 1)) is empty ) ) ;

suppose A12: ( IT is empty or dom (H . (n + 1)) is empty ) ; :: thesis: { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } is finite

{ (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } = {}

proof

assume { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A13: x in { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } by XBOOLE_0:def 1;
ex f being Element of IT ex i being Element of dom (H . (n + 1)) st
( x = f ^ <*i*> & f in IT & i in dom (H . (n + 1)) ) by A13;
hence contradiction by A12; :: thesis: verum

end;

hence { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } is finite ; :: thesis: verum

end;

suppose A14: ( not IT is empty & not dom (H . (n + 1)) is empty ) ; :: thesis: { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } is finite

then reconsider ITn = IT as non empty FinSequence-membered set ;
reconsider D = dom (H . (n + 1)) as non empty set by A14;
deffunc H₁( FinSequence, object ) -> set = $1 ^ <*$2*>;
set Pfi = { H₁(f,i) where f is Element of ITn, i is Element of D : ( f in ITn & i in D ) } ;
A15: D is finite ;
A16: ITn is finite ;
{ H₁(f,i) where f is Element of ITn, i is Element of D : ( f in ITn & i in D ) } is finite from FRAENKEL:sch 22(A16, A15);
hence { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } is finite ; :: thesis: verum

end;

end;

end;

now :: thesis: for x being object st x in { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } holds
x is FinSequence

let x be object ; :: thesis: ( x in { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } implies x is FinSequence )
assume x in { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } ; :: thesis: x is FinSequence
then ex f being Element of IT ex i being Element of dom (H . (n + 1)) st
( x = f ^ <*i*> & f in IT & i in dom (H . (n + 1)) ) ;
hence x is FinSequence ; :: thesis: verum

end;

then reconsider IT2 = { (f ^ <*i*>) where f is Element of IT, i is Element of dom (H . (n + 1)) : ( f in IT & i in dom (H . (n + 1)) ) } as finite FinSequence-membered set by A11, FINSEQ_1:def 19;
take IT2 ; :: thesis: for x being object holds
( x in IT2 iff S₁[x,H] )
let x be object ; :: thesis: ( x in IT2 iff S₁[x,H] )
thus ( x in IT2 implies S₁[x,H] ) :: thesis: ( S₁[x,H] implies x in IT2 )

proof

assume x in IT2 ; :: thesis: S₁[x,H]
then consider fs being Element of IT, i being Element of dom (H . (n + 1)) such that
A17: ( x = fs ^ <*i*> & fs in IT & i in dom (H . (n + 1)) ) ;
consider f being FinSequence such that
A18: ( f = fs & len f = len Hn & ( for i being Nat st i in dom f holds
f . i in dom (Hn . i) ) ) by A17, A10;
take fH = f ^ <*i*>; :: thesis: ( fH = x & len fH = len H & ( for i being Nat st i in dom fH holds
fH . i in dom (H . i) ) )
thus A19: ( fH = x & len fH = len H ) by A7, A18, A17, A9, FINSEQ_2:16; :: thesis: for i being Nat st i in dom fH holds
fH . i in dom (H . i)
let k be Nat; :: thesis: ( k in dom fH implies fH . k in dom (H . k) )
assume A20: k in dom fH ; :: thesis: fH . k in dom (H . k)
A21: ( 1 <= k & k <= n + 1 ) by A7, A20, A19, FINSEQ_3:25;

per cases ( k <= n or k = n + 1 ) by A21, NAT_1:8;

suppose A22: k <= n ; :: thesis: fH . k in dom (H . k)

then A23: ( k in dom f & k in dom Hn ) by A21, A18, A9, FINSEQ_3:25;
A24: f . k in dom (Hn . k) by A22, A21, A18, A9, FINSEQ_3:25;
Hn . k = H . k by FINSEQ_3:112, A22;
hence fH . k in dom (H . k) by A24, A23, FINSEQ_1:def 7; :: thesis: verum

end;

suppose k = n + 1 ; :: thesis: fH . k in dom (H . k)

hence fH . k in dom (H . k) by A17, A18, A9; :: thesis: verum

end;

end;

end;

given p being FinSequence such that A25: ( p = x & len p = len H & ( for i being Nat st i in dom p holds
p . i in dom (H . i) ) ) ; :: thesis: x in IT2
set pn = p | n;
A26: ( p = p | (len p) & p | (len p) = (p | n) ^ <*(p . (n + 1))*> ) by A7, A8, A25, FINSEQ_5:83;
A27: len (p | n) = len Hn by A9, A25, NAT_1:11, FINSEQ_1:59, A7;
for i being Nat st i in dom (p | n) holds
(p | n) . i in dom (Hn . i)

proof

let i be Nat; :: thesis: ( i in dom (p | n) implies (p | n) . i in dom (Hn . i) )
assume A28: i in dom (p | n) ; :: thesis: (p | n) . i in dom (Hn . i)
A29: i <= n by A28, A27, A9, FINSEQ_3:25;
A30: dom (p | n) c= dom p by FINSEQ_5:18;
( (p | n) . i = p . i & Hn . i = H . i ) by A29, FINSEQ_3:112;
hence (p | n) . i in dom (Hn . i) by A30, A28, A25; :: thesis: verum

end;

then A31: p | n in IT by A27, A10;
p . (n + 1) in dom (H . (n + 1)) by A25, A8, A7, FINSEQ_3:25;
hence x in IT2 by A25, A26, A31; :: thesis: verum

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A1, A5);
then consider IT being finite FinSequence-membered set such that
A32: for x being object holds
( x in IT iff S₁[x,F] ) ;
IT c= NAT *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IT or x in NAT * )
assume x in IT ; :: thesis: x in NAT *
then consider p being FinSequence such that
A33: ( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) by A32;
rng p c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in NAT )
assume y in rng p ; :: thesis: y in NAT
then consider x being object such that
A34: ( x in dom p & p . x = y ) by FUNCT_1:def 3;
p . x in dom (F . x) by A34, A33;
hence y in NAT by A34; :: thesis: verum

end;

then p is FinSequence of NAT by FINSEQ_1:def 4;
hence x in NAT * by FINSEQ_1:def 11, A33; :: thesis: verum

end;

hence ex b₁ being finite Subset of (NAT *) st
for x being object holds
( x in b₁ iff ex p being FinSequence st
( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) ) by A32; :: thesis: verum