A1: { s where s is Element of T : not t is_a_proper_prefix_of s } c= T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of T : not t is_a_proper_prefix_of s } or x in T )
assume x in { s where s is Element of T : not t is_a_proper_prefix_of s } ; :: thesis: x in T
then ex s being Element of T st
( x = s & not t is_a_proper_prefix_of s ) ;
hence x in T ; :: thesis: verum

end;

T1,{ (t ^ s) where s is Element of T1 : s = s } are_equipotent

proof

defpred S₁[ set , set ] means ex q being FinSequence of NAT st
( T = q & t = t ^ q );
A5: for x being set st x in T1 holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in T1 implies ex y being set st S₁[x,y] )
assume x in T1 ; :: thesis: ex y being set st S₁[x,y]
then reconsider q = x as FinSequence of NAT by Th44;
t ^ q = t ^ q ;
hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

consider f being Function such that
A8: ( dom f = T1 & ( for x being set st x in T1 holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A5);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = T1 & proj2 f = { (t ^ s) where s is Element of T1 : s = s } )
thus f is one-to-one :: thesis: ( proj1 f = T1 & proj2 f = { (t ^ s) where s is Element of T1 : s = s } )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A9: ( x in dom f & y in dom f ) and
A10: f . x = f . y ; :: thesis: x = y
( ex q being FinSequence of NAT st
( x = q & f . x = t ^ q ) & ex r being FinSequence of NAT st
( y = r & f . y = t ^ r ) ) by A8, A9;
hence x = y by A10, FINSEQ_1:46; :: thesis: verum

end;

thus dom f = T1 by A8; :: thesis: proj2 f = { (t ^ s) where s is Element of T1 : s = s }
thus rng f c= { (t ^ s) where s is Element of T1 : s = s } :: according to XBOOLE_0:def 10 :: thesis: { (t ^ s) where s is Element of T1 : s = s } is_a_prefix_of proj2 f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in { (t ^ s) where s is Element of T1 : s = s } )
assume x in rng f ; :: thesis: x in { (t ^ s) where s is Element of T1 : s = s }
then consider y being set such that
A13: y in dom f and
A14: x = f . y by FUNCT_1:def 5;
consider q being FinSequence of NAT such that
A15: y = q and
A16: f . y = t ^ q by A8, A13;
reconsider q = q as Element of T1 by A8, A13, A15;
x = t ^ q by A14, A16;
hence x in { (t ^ s) where s is Element of T1 : s = s } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ s) where s is Element of T1 : s = s } or x in proj2 f )
assume x in { (t ^ s) where s is Element of T1 : s = s } ; :: thesis: x in proj2 f
then consider s being Element of T1 such that
A19: x = t ^ s and
s = s ;
S₁[s,f . s] by A8;
hence x in proj2 f by A8, A19, FUNCT_1:def 5; :: thesis: verum

end;

then { (t ^ s) where s is Element of T1 : s = s } is finite by CARD_1:68;
then { v where v is Element of T : not t is_a_proper_prefix_of v } \/ { (t ^ s) where s is Element of T1 : s = s } is finite by A1;
hence T with-replacement t,T1 is finite by Th64; :: thesis: verum