let C be non empty set ; :: thesis: 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

let f be sequence of C; :: thesis: 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

let X be finite set ; :: thesis: ( ( 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) implies ex k being Nat st X c= f . k )

assume that
A1: for n, m being Nat st m in dom f & n in dom f & n < m holds
f . n c= f . m and
A2: X c= union (rng f) ; :: thesis: ex k being Nat st X c= f . k
A3: now :: thesis: ( not X is empty implies ex a being Nat st X c= f . a )
deffunc H1( object ) -> Element of omega = min* { i where i is Nat : \$1 in f . i } ;
consider g being Function such that
A4: ( dom g = X & ( for a being object st a in X holds
g . a = H1(a) ) ) from reconsider A = rng g as finite set by ;
A5: now :: thesis: for b being object st b in A holds
b in NAT
let b be object ; :: thesis: ( b in A implies b in NAT )
assume b in A ; :: thesis:
then consider a being object such that
A6: ( a in dom g & g . a = b ) by FUNCT_1:def 3;
b = min* { i where i is Nat : a in f . i } by A4, A6;
hence b in NAT ; :: thesis: verum
end;
assume not X is empty ; :: thesis: ex a being Nat st X c= f . a
then ex c being object st c in dom g by A4;
then reconsider A = A as non empty finite Subset of NAT by ;
union A in A by Th2;
then reconsider a = union A as Nat ;
take a = a; :: thesis: X c= f . a
thus X c= f . a :: thesis: verum
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in X or b in f . a )
assume A7: b in X ; :: thesis: b in f . a
then consider c being set such that
A8: b in c and
A9: c in rng f by ;
consider d being object such that
A10: d in dom f and
A11: f . d = c by ;
reconsider d = d as Nat by A10;
d in { i where i is Nat : b in f . i } by ;
then reconsider Y = { i where i is Nat : b in f . i } as non empty set ;
now :: thesis: for a being object st a in Y holds
a in NAT
let a be object ; :: thesis: ( a in Y implies a in NAT )
assume a in Y ; :: thesis:
then ex i being Nat st
( i = a & b in f . i ) ;
hence a in NAT by ORDINAL1:def 12; :: thesis: verum
end;
then reconsider Y = Y as non empty Subset of NAT by TARSKI:def 3;
A12: g . b = min* Y by A4, A7;
then reconsider Y9 = g . b as Nat ;
Y9 in Y by ;
then A13: ex i being Nat st
( i = g . b & b in f . i ) ;
A14: dom f = NAT by FUNCT_2:def 1;
A15: now :: thesis: ( Y9 in a implies b in f . a )
assume Y9 in a ; :: thesis: b in f . a
then Y9 in { k where k is Nat : k < a } by AXIOMS:4;
then consider k being Nat such that
A16: ( k = Y9 & k < a ) ;
A17: a in NAT by ORDINAL1:def 12;
Y9 in NAT by ORDINAL1:def 12;
then f . Y9 c= f . a by A1, A14, A16, A17;
hence b in f . a by A13; :: thesis: verum
end;
Y9 in A by ;
hence b in f . a by ; :: thesis: verum
end;
end;
now :: thesis: ( X is empty implies ex k being Element of omega ex k being Nat st X c= f . k )
assume A18: X is empty ; :: thesis: ex k being Element of omega ex k being Nat st X c= f . k
take k = 0 ; :: thesis: ex k being Nat st X c= f . k
{} c= f . k ;
hence ex k being Nat st X c= f . k by A18; :: thesis: verum
end;
hence ex k being Nat st X c= f . k by A3; :: thesis: verum