let E be non empty finite set ; :: thesis: for ASeq being SetSequence of E st ASeq is non-descending holds
ex N being Nat st
for m being Nat st N <= m holds
ASeq . N = ASeq . m
let ASeq be SetSequence of E; :: thesis: ( ASeq is non-descending implies ex N being Nat st
for m being Nat st N <= m holds
ASeq . N = ASeq . m )
defpred S₁[ Element of NAT , set ] means $2 = card (ASeq . $1);
A1: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[x,y]
card (ASeq . x) in REAL by NUMBERS:19;
hence ex y being Element of REAL st S₁[x,y] ; :: thesis: verum

end;

consider seq being sequence of REAL such that
A2: for n being Element of NAT holds S₁[n,seq . n] from FUNCT_2:sch 3(A1);

now :: thesis: for n being Nat holds seq . n < (card E) + 1

let n be Nat; :: thesis: seq . n < (card E) + 1
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
card (ASeq . nn) <= card E by NAT_1:43;
then card (ASeq . nn) < (card E) + 1 by NAT_1:13;
hence seq . n < (card E) + 1 by A2; :: thesis: verum

end;

then A3: seq is bounded_above by SEQ_2:def 3;
assume A4: ASeq is non-descending ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
ASeq . N = ASeq . m

A5: now :: thesis: for n, m being Nat st n <= m holds
seq . n <= seq . m

let n, m be Nat; :: thesis: ( n <= m implies seq . n <= seq . m )
reconsider mm = m, nn = n as Element of NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: seq . n <= seq . m
then A6: ASeq . n c= ASeq . m by A4, PROB_1:def 5;
( seq . mm = card (ASeq . mm) & seq . nn = card (ASeq . nn) ) by A2;
hence seq . n <= seq . m by A6, NAT_1:43; :: thesis: verum

end;

then seq is non-decreasing by SEQM_3:6;
then consider g being Real such that
A7: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p by A3, SEQ_2:def 6;
consider N being Nat such that
A8: for m being Nat st N <= m holds
|.((seq . m) - g).| < 1 / 2 by A7;
take N ; :: thesis: for m being Nat st N <= m holds
ASeq . N = ASeq . m

now :: thesis: for m being Nat st N <= m holds
ASeq . m = ASeq . N

|.((seq . N) - g).| < 1 / 2 by A8;
then A9: |.(g - (seq . N)).| < 1 / 2 by COMPLEX1:60;
let m be Nat; :: thesis: ( N <= m implies ASeq . m = ASeq . N )
reconsider NN = N, mm = m as Element of NAT by ORDINAL1:def 12;
A10: ( seq . NN = card (ASeq . NN) & seq . mm = card (ASeq . mm) ) by A2;
assume A11: N <= m ; :: thesis: ASeq . m = ASeq . N
then A12: ( seq . N <= seq . m & ASeq . N c= ASeq . m ) by A4, A5, PROB_1:def 5;
|.((seq . m) - g).| < 1 / 2 by A8, A11;
then A13: |.((seq . m) - g).| + |.(g - (seq . N)).| < (1 / 2) + (1 / 2) by A9, XREAL_1:8;
|.((seq . m) - (seq . N)).| <= |.((seq . m) - g).| + |.(g - (seq . N)).| by COMPLEX1:63;
then |.((seq . m) - (seq . N)).| < 1 by A13, XXREAL_0:2;
then (seq . m) - (seq . N) < 1 by ABSVALUE:def 1;
then ((seq . m) - (seq . N)) + (seq . N) < 1 + (seq . N) by XREAL_1:8;
then seq . m <= seq . N by A10, NAT_1:8;
hence ASeq . m = ASeq . N by A10, A12, CARD_2:102, XXREAL_0:1; :: thesis: verum

end;

hence for m being Nat st N <= m holds
ASeq . N = ASeq . m ; :: thesis: verum