let E be non empty finite set ; 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; ( ASeq is non-descending implies ex N being Nat st
for m being Nat st N <= m holds
ASeq . N = ASeq . m )
defpred S1[ Element of NAT , set ] means $2 = card (ASeq . $1);
A1:
for x being Element of NAT ex y being Element of REAL st S1[x,y]
consider seq being sequence of REAL such that
A2:
for n being Element of NAT holds S1[n,seq . n]
from FUNCT_2:sch 3(A1);
then A3:
seq is V138()
by SEQ_2:def 3;
assume A4:
ASeq is non-descending
; ex N being Nat st
for m being Nat st N <= m holds
ASeq . N = ASeq . m
A5:
now for n, m being Nat st n <= m holds
seq . n <= seq . mend;
then
seq is V74()
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
; for m being Nat st N <= m holds
ASeq . N = ASeq . m
now 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;
( 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
;
ASeq . m = ASeq . Nthen 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;
verum end;
hence
for m being Nat st N <= m holds
ASeq . N = ASeq . m
; verum