consider n being Nat such that
A1: T, Seg n are_equipotent by FINSEQ_1:77;
defpred S₁[ Nat] means for p being FinSequence of NAT st p in T holds
len p <= $1;
A2: ex n being Nat st S₁[n]

proof

now

given p being FinSequence of NAT such that A3: ( p in T & not len p <= n ) ; :: thesis: contradiction
( ProperPrefixes p c= T & ProperPrefixes p, dom p are_equipotent ) by A3, Def5, Th67;
then A4: ( card (ProperPrefixes p) c= card T & card T = card (Seg n) & card (ProperPrefixes p) = card (dom p) ) by A1, CARD_1:21, CARD_1:27;
A5: dom p = Seg (len p) by FINSEQ_1:def 3;
Seg n c= Seg (len p) by A3, FINSEQ_1:7;
then ( card (Seg n) c= card (Seg (len p)) & card (Seg n) = card n & card (Seg (len p)) = card (len p) ) by CARD_1:27, FINSEQ_1:76;
then card n = card (len p) by A4, A5, XBOOLE_0:def 10;
hence contradiction by A3, CARD_1:71; :: thesis: verum

end;

then consider n being Nat such that
A6: S₁[n] ;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
take n ; :: thesis: S₁[n]
thus S₁[n] by A6; :: thesis: verum

end;

consider n being Nat such that
A7: S₁[n] and
A8: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A2);
consider x being Element of T;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
take n ; :: thesis: ( ex p being FinSequence of NAT st
( p in T & len p = n ) & ( for p being FinSequence of NAT st p in T holds
len p <= n ) )
thus ex p being FinSequence of NAT st
( p in T & len p = n ) :: thesis: for p being FinSequence of NAT st p in T holds
len p <= n

proof

assume A9: for p being FinSequence of NAT st p in T holds
len p <> n ; :: thesis: contradiction
reconsider x = x as FinSequence of NAT ;
( len x <> n & len x <= n ) by A7, A9;
then ( 0 <= len x & len x < n ) by XXREAL_0:1;
then consider k being Nat such that
A10: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
for p being FinSequence of NAT st p in T holds
len p <= k

proof

let p be FinSequence of NAT ; :: thesis: ( p in T implies len p <= k )
assume p in T ; :: thesis: len p <= k
then ( len p <= n & len p <> n ) by A7, A9;
then len p < k + 1 by A10, XXREAL_0:1;
hence len p <= k by NAT_1:13; :: thesis: verum

end;

then n <= k by A8;
hence contradiction by A10, NAT_1:13; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: ( p in T implies len p <= n )
assume p in T ; :: thesis: len p <= n
hence len p <= n by A7; :: thesis: verum