consider n being Nat such that
A1: T, Seg n are_equipotent by FINSEQ_1:56;
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 :: thesis: for p being FinSequence of NAT holds
( not p in T or len p <= n )

given p being FinSequence of NAT such that A3: p in T and
A4: not len p <= n ; :: thesis: contradiction
A5: ProperPrefixes p c= T by A3, Def3;
A6: ProperPrefixes p, dom p are_equipotent by Th33;
A7: card (ProperPrefixes p) c= card T by A5, CARD_1:11;
A8: card (ProperPrefixes p) = card (dom p) by A6, CARD_1:5;
A9: ( card T = card (Seg n) & dom p = Seg (len p) ) by A1, CARD_1:5, FINSEQ_1:def 3;
Seg n c= Seg (len p) by A4, FINSEQ_1:5;
then A10: card (Seg n) c= card (Seg (len p)) by CARD_1:11;
( card (Seg n) = card n & card (Seg (len p)) = card (len p) ) by FINSEQ_1:55;
then card n = card (len p) by A7, A8, A9, A10;
hence contradiction by A4; :: thesis: verum

end;

then consider n being Nat such that
A11: S₁[n] ;
reconsider n = n as Nat ;
take n ; :: thesis: S₁[n]
thus S₁[n] by A11; :: thesis: verum

end;

consider n being Nat such that
A12: S₁[n] and
A13: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A2);
set x = the Element of T;
reconsider n = n as Nat ;
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 A14: for p being FinSequence of NAT st p in T holds
len p <> n ; :: thesis: contradiction
reconsider x = the Element of T as FinSequence of NAT ;
len x <= n by A12;
then len x < n by A14, XXREAL_0:1;
then consider k being Nat such that
A15: n = k + 1 by NAT_1:6;
reconsider k = k as Nat ;
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 A16: p in T ; :: thesis: len p <= k
then len p <= n by A12;
then len p < k + 1 by A14, A15, A16, XXREAL_0:1;
hence len p <= k by NAT_1:13; :: thesis: verum

end;

then n <= k by A13;
hence contradiction by A15, 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 A12; :: thesis: verum