let E be non empty finite set ; :: thesis: for ASeq being SetSequence of E st ASeq is non-ascending holds
ex N being Element of NAT st
for m being Element of NAT st N <= m holds
ASeq . N = ASeq . m
let ASeq be SetSequence of E; :: thesis: ( ASeq is non-ascending implies ex N being Element of NAT st
for m being Element of NAT st N <= m holds
ASeq . N = ASeq . m )
assume A1: ASeq is non-ascending ; :: thesis: ex N being Element of NAT st
for m being Element of NAT st N <= m holds
ASeq . N = ASeq . m
defpred S₁[ Element of NAT , set ] means $2 = card (ASeq . $1);
P1: 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 NAT ;
hence ex y being Element of REAL st S₁[x,y] ; :: thesis: verum

end;

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

PP3: now

let n, m be Element of NAT ; :: thesis: ( n <= m implies seq . m <= seq . n )
assume n <= m ; :: thesis: seq . m <= seq . n
then P21: ASeq . m c= ASeq . n by A1, PROB_1:def 6;
( seq . m = card (ASeq . m) & seq . n = card (ASeq . n) ) by P2;
hence seq . m <= seq . n by P21, NAT_1:44; :: thesis: verum

end;

then P3: seq is V51() by SEQM_3:14;

now

let m be Element of NAT ; :: thesis: - 1 < seq . m
seq . m = card (ASeq . m) by P2;
hence - 1 < seq . m ; :: thesis: verum

end;

then seq is bounded_below by SEQ_2:def 4;
then consider g being real number such that
P4: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p by P3, SEQ_2:def 6;
consider N being Element of NAT such that
P5: for m being Element of NAT st N <= m holds
abs ((seq . m) - g) < 1 / 2 by P4;
take N ; :: thesis: for m being Element of NAT st N <= m holds
ASeq . N = ASeq . m

now

let m be Element of NAT ; :: thesis: ( N <= m implies ASeq . m = ASeq . N )
assume P6: N <= m ; :: thesis: ASeq . m = ASeq . N
then P7: abs ((seq . m) - g) < 1 / 2 by P5;
abs ((seq . N) - g) < 1 / 2 by P5;
then abs (g - (seq . N)) < 1 / 2 by COMPLEX1:146;
then P71: (abs ((seq . m) - g)) + (abs (g - (seq . N))) < (1 / 2) + (1 / 2) by P7, XREAL_1:10;
abs ((seq . m) - (seq . N)) <= (abs ((seq . m) - g)) + (abs (g - (seq . N))) by COMPLEX1:149;
then P72: abs ((seq . m) - (seq . N)) < 1 by P71, XXREAL_0:2;
X1: seq . N = card (ASeq . N) by P2;
X2: seq . m = card (ASeq . m) by P2;
P75: seq . m <= seq . N by PP3, P6;
PP81: ASeq . m c= ASeq . N by P6, A1, PROB_1:def 6;
abs ((seq . N) - (seq . m)) < 1 by P72, COMPLEX1:146;
then (seq . N) - (seq . m) < 1 by ABSVALUE:def 1;
then ((seq . N) - (seq . m)) + (seq . m) < 1 + (seq . m) by XREAL_1:10;
then seq . N <= seq . m by X1, X2, NAT_1:8;
hence ASeq . m = ASeq . N by PP81, CARD_FIN:1, X1, X2, P75, XXREAL_0:1; :: thesis: verum

end;

hence for m being Element of NAT st N <= m holds
ASeq . N = ASeq . m ; :: thesis: verum