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

A3: 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;
A11: Seg n c= Seg (len p) by A5, FINSEQ_1:7;
A12: card (Seg n) c= card (Seg (len p)) by A11, CARD_1:27;
A13: ( card (Seg n) = card n & card (Seg (len p)) = card (len p) ) by FINSEQ_1:76;
A14: card n = card (len p) by A8, A9, A10, A12, A13, XBOOLE_0:def 10;
thus contradiction by A5, A14, CARD_1:71; :: thesis: verum

end;

consider n being Nat such that
A15: S₁[n] by A3;
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 ;
A19: len x <= n by A16;
A20: len x < n by A18, A19, XXREAL_0:1;
consider k being Nat such that
A21: n = k + 1 by A20, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A22: 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
A24: len p <= n by A16, A23;
A25: len p < k + 1 by A18, A21, A23, A24, XXREAL_0:1;
thus len p <= k by A25, NAT_1:13; :: thesis: verum

end;

A26: n <= k by A17, A22;
thus contradiction by A21, A26, NAT_1:13; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: ( p in T implies len p <= n )
assume A27: p in T ; :: thesis: len p <= n
thus len p <= n by A16, A27; :: thesis: verum