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]

let x be object ; :: thesis:
assume x in dom t ; :: thesis:
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:

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

take f ; :: according to FINSET_1:def 1 :: thesis:
thus rng f c= T | p :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
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:
( 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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in T | p ; :: thesis:
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:

end;

end;

hence T | p is finite ; :: thesis: