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 ) ) );
A3: 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
A7: ( dom f = dom t & ( for x being set st x in dom t holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A3);
T | p is finite

proof

take f ; :: according to FINSET_1:def 1 :: thesis: ( proj2 f = T | p & proj1 f in NAT )
thus rng f c= T | p :: according to XBOOLE_0:def 10 :: thesis: ( T | p is_a_prefix_of proj2 f & proj1 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
A10: y in dom f and
A11: x = f . y by FUNCT_1:def 5;
consider q being FinSequence of NAT such that
A12: t . y = q and
A13: ( 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 A7, A10, A11;
assume A14: not x in T | p ; :: thesis: contradiction
( p ^ (<*> NAT) = p & q in T ) by A1, A7, A10, A12, FINSEQ_1:47, FUNCT_1:def 5;
hence contradiction by A13, A14, Def9; :: thesis: verum

end;

thus T | p c= rng f :: thesis: proj1 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 A16: x in T | p ; :: thesis: x in rng f
then reconsider q = x as FinSequence of NAT by Th44;
p ^ q in T by A16, Def9;
then consider y being set such that
A18: y in dom t and
A19: p ^ q = t . y by A1, FUNCT_1:def 5;
S₁[y,f . y] by A7, A18;
then x = f . y by A19, FINSEQ_1:46;
hence x in rng f by A7, A18, FUNCT_1:def 5; :: thesis: verum

end;

thus proj1 f in NAT by A2, A7; :: thesis: verum

end;

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