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 A4: x in dom t ; :: thesis: ex y being set st S₁[x,y]
A5: t . x in T by A1, A4, FUNCT_1:def 5;
reconsider q = t . x as FinSequence of NAT by A5, Th44;
A6: ( ex r being FinSequence of NAT st q = p ^ r implies ex y being set st S₁[x,y] ) ;
thus ex y being set st S₁[x,y] by A6; :: 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);
A8: 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 A9: x in rng f ; :: thesis: x in T | p
consider y being set such that
A10: y in dom f and
A11: x = f . y by A9, 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
A15: ( p ^ (<*> NAT ) = p & q in T ) by A1, A7, A10, A12, FINSEQ_1:47, FUNCT_1:def 5;
thus contradiction by A13, A14, A15, 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
reconsider q = x as FinSequence of NAT by A16, Th44;
A17: p ^ q in T by A16, Def9;
consider y being set such that
A18: y in dom t and
A19: p ^ q = t . y by A1, A17, FUNCT_1:def 5;
A20: S₁[y,f . y] by A7, A18;
A21: x = f . y by A19, A20, FINSEQ_1:46;
thus x in rng f by A7, A18, A21, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

thus T | p is finite by A8; :: thesis: verum