consider t being Function such that
A1: rng t = T and
A2: dom t in omega by FINSET_1:def 1;
defpred S₁[ object , object ] 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 object st x in dom t holds
ex y being object st S₁[x,y]

proof

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

end;

consider f being Function such that
A4: ( dom f = dom t & ( for x being object 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: ( rng f = T | p & dom f in omega )
thus rng f c= T | p :: according to XBOOLE_0:def 10 :: thesis: ( T | p is_a_prefix_of rng f & dom f in omega )

proof

let x be object ; :: 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 object such that
A5: y in dom f and
A6: x = f . y by FUNCT_1:def 3;
consider q being FinSequence of NAT such that
A7: t . y = q and
A8: ( 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 A4, A5, A6;
assume A9: not x in T | p ; :: thesis: contradiction
( p ^ (<*> NAT) = p & q in T ) by A1, A4, A5, A7, FINSEQ_1:34, FUNCT_1:def 3;
hence contradiction by A8, A9, Def6; :: thesis: verum

end;

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

proof

let x be object ; :: 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 Th18;
p ^ q in T by A10, Def6;
then consider y being object such that
A11: y in dom t and
A12: p ^ q = t . y by A1, FUNCT_1:def 3;
S₁[y,f . y] by A4, A11;
then x = f . y by A12, FINSEQ_1:33;
hence x in rng f by A4, A11, FUNCT_1:def 3; :: thesis: verum

end;

thus dom f in omega by A2, A4; :: thesis: verum

end;

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