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 A4: p in T and
A5: not len p <= n ; :: thesis: contradiction
A6: ProperPrefixes p c= T by A4, Def5;
A7: ProperPrefixes p, dom p are_equipotent by Th67;
A8: card (ProperPrefixes p) c= card T by A6, CARD_1:27;
A9: card (ProperPrefixes p) = card (dom p) by A7, CARD_1:21;
A10: ( card T = card (Seg n) & dom p = Seg (len p) ) by A1, CARD_1:21, FINSEQ_1:def 3;
Seg n c= Seg (len p) by A5, FINSEQ_1:7;
then A12: card (Seg n) c= card (Seg (len p)) by CARD_1:27;
( card (Seg n) = card n & card (Seg (len p)) = card (len p) ) by FINSEQ_1:76;
then card n = card (len p) by A8, A9, A10, A12, XBOOLE_0:def 10;
hence contradiction by A5, CARD_1:71; :: thesis: verum

end;

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

end;

consider n being Nat such that
A16: S₁[n] and
A17: 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 A18: 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 by A16;
then len x < n by A18, XXREAL_0:1;
then consider k being Nat such that
A21: 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 A23: p in T ; :: thesis: len p <= k
then len p <= n by A16;
then len p < k + 1 by A18, A21, A23, XXREAL_0:1;
hence len p <= k by NAT_1:13; :: thesis: verum

end;

then n <= k by A17;
hence contradiction by A21, 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 A16; :: thesis: verum