let X be non empty set ; :: thesis: for F being SetSequence of X st F is non-ascending holds
for S being Function of NAT,X st ( for n being natural number holds S . n in F . n ) & rng S is finite holds
not meet F is empty
let F be SetSequence of X; :: thesis: ( F is non-ascending implies for S being Function of NAT,X st ( for n being natural number holds S . n in F . n ) & rng S is finite holds
not meet F is empty )
assume A1: F is non-ascending ; :: thesis: for S being Function of NAT,X st ( for n being natural number holds S . n in F . n ) & rng S is finite holds
not meet F is empty
let S be Function of NAT,X; :: thesis: ( ( for n being natural number holds S . n in F . n ) & rng S is finite implies not meet F is empty )
assume A2: for n being natural number holds S . n in F . n ; :: thesis: ( not rng S is finite or not meet F is empty )
A3: dom S = NAT by FUNCT_2:def 1;
assume rng S is finite ; :: thesis: not meet F is empty
then consider x being set such that
x in rng S and
A4: not S " {x} is finite by A3, Th24;

now

let n be Element of NAT ; :: thesis: x in F . n
ex i being natural number st
( x in F . i & i >= n )

proof

assume A5: for i being natural number st x in F . i holds
i < n ; :: thesis: contradiction
S " {x} c= n

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in S " {x} or y in n )
assume A6: y in S " {x} ; :: thesis: y in n
reconsider i = y as Element of NAT by A6;
S . i in {x} by A6, FUNCT_1:def 7;
then A7: S . i = x by TARSKI:def 1;
S . i in F . i by A2;
then i < n by A5, A7;
hence y in n by NAT_1:44; :: thesis: verum

end;

hence contradiction by A4; :: thesis: verum

end;

then consider i being natural number such that
A8: x in F . i and
A9: i >= n ;
i in NAT by ORDINAL1:def 12;
then F . i c= F . n by A1, A9, PROB_1:def 4;
hence x in F . n by A8; :: thesis: verum

end;

hence not meet F is empty by KURATO_0:3; :: thesis: verum