for C being non empty set
for f being sequence of C
for X being finite set st ( for n, m being Nat st m in dom f & n in dom f & n < m holds
f . n c= f . m ) & X c= union (rng f) holds
ex k being Nat st X c= f . k