consider t being Function such that
A1: rng t = T and
A2: dom t in omega by FINSET_1:def 1;
defpred S₁[ set , set ] means ex q being FinSequence of NAT st
( t . T = q & ( ex r being FinSequence of NAT st
( p = r & q = p ^ r ) or ( ( for r being FinSequence of NAT holds q <> p ^ r ) & p = <*> NAT ) ) );
A4: for x being set st x in dom t holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in dom t implies ex y being set st S₁[x,y] )
assume x in dom t ; :: thesis: ex y being set st S₁[x,y]
then t . x in T by A1, FUNCT_1:def 5;
then reconsider q = t . x as FinSequence of NAT by Th44;
( ex r being FinSequence of NAT st q = p ^ r implies ex y being set st S₁[x,y] ) ;
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A5: ( dom f = dom t & ( for x being set st x in dom t holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A4);
T | p is finite

proof

take f ; :: according to FINSET_1:def 1 :: thesis: ( rng f = T | p & dom f in NAT )
thus rng f c= T | p :: according to XBOOLE_0:def 10 :: thesis: ( T | p is_a_prefix_of rng f & dom f in NAT )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in T | p )
assume x in rng f ; :: thesis: x in T | p
then consider y being set such that
A6: ( y in dom f & x = f . y ) by FUNCT_1:def 5;
consider q being FinSequence of NAT such that
A7: ( t . y = q & ( ex r being FinSequence of NAT st
( x = r & q = p ^ r ) or ( ( for r being FinSequence of NAT holds q <> p ^ r ) & x = <*> NAT ) ) ) by A5, A6;
A8: p ^ (<*> NAT ) = p by FINSEQ_1:47;
assume A9: not x in T | p ; :: thesis: contradiction
( q in T & p in T ) by A1, A5, A6, A7, FUNCT_1:def 5;
hence contradiction by A7, A8, A9, Def9; :: thesis: verum

end;

thus T | p c= rng f :: thesis: dom f in NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T | p or x in rng f )
assume A10: x in T | p ; :: thesis: x in rng f
then reconsider q = x as FinSequence of NAT by Th44;
p ^ q in T by A10, Def9;
then consider y being set such that
A11: ( y in dom t & p ^ q = t . y ) by A1, FUNCT_1:def 5;
S₁[y,f . y] by A5, A11;
then x = f . y by A11, FINSEQ_1:46;
hence x in rng f by A5, A11, FUNCT_1:def 5; :: thesis: verum

end;

thus dom f in NAT by A2, A5; :: thesis: verum

end;

hence T | p is finite ; :: thesis: verum