let C be non empty set ; :: thesis: for f being Function of NAT ,C
for X being finite set st ( for n, m being Element of 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 Element of NAT st X c= f . k
let f be Function of NAT ,C; :: thesis: for X being finite set st ( for n, m being Element of 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 Element of NAT st X c= f . k
let X be finite set ; :: thesis: ( ( for n, m being Element of 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 Element of NAT st X c= f . k )
assume that
A1: for n, m being Element of 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 Element of NAT st X c= f . k

A3: now

deffunc H₁( set ) -> Element of NAT = min* { i where i is Element of NAT : $1 in f . i } ;
consider g being Function such that
A4: ( dom g = X & ( for a being set st a in X holds
g . a = H₁(a) ) ) from FUNCT_1:sch 3();
reconsider A = rng g as finite set by A4, FINSET_1:26;

A5: now

let b be set ; :: thesis: ( b in A implies b in NAT )
assume b in A ; :: thesis: b in NAT
then consider a being set such that
A6: ( a in dom g & g . a = b ) by FUNCT_1:def 5;
b = min* { i where i is Element of NAT : a in f . i } by A4, A6;
hence b in NAT ; :: thesis: verum

end;

assume not X is empty ; :: thesis: ex a being Element of NAT st X c= f . a
then ex c being set st c in dom g by A4, XBOOLE_0:def 1;
then reconsider A = A as non empty finite Subset of NAT by A5, FUNCT_1:12, TARSKI:def 3;
union A in A by Th2;
then reconsider a = union A as Element of NAT ;
take a = a; :: thesis: X c= f . a
thus X c= f . a :: thesis: verum

proof

let b be set ; :: 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 A2, TARSKI:def 4;
consider d being set such that
A10: d in dom f and
A11: f . d = c by A9, FUNCT_1:def 5;
reconsider d = d as Element of NAT by A10;
d in { i where i is Element of NAT : b in f . i } by A8, A11;
then reconsider Y = { i where i is Element of NAT : b in f . i } as non empty set ;

now

let a be set ; :: thesis: ( a in Y implies a in NAT )
assume a in Y ; :: thesis: a in NAT
then ex i being Element of NAT st
( i = a & b in f . i ) ;
hence a in NAT ; :: 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 Element of NAT ;
Y9 in Y by A12, NAT_1:def 1;
then A13: ex i being Element of NAT st
( i = g . b & b in f . i ) ;
A14: dom f = NAT by FUNCT_2:def 1;

A15: now

assume Y9 in a ; :: thesis: b in f . a
then Y9 in { k where k is Element of NAT : k < a } by AXIOMS:30;
then ex k being Element of NAT st
( k = Y9 & k < a ) ;
then f . Y9 c= f . a by A1, A14;
hence b in f . a by A13; :: thesis: verum

end;

Y9 in A by A4, A7, FUNCT_1:12;
hence b in f . a by A13, A15, Th2; :: thesis: verum

end;

end;

now

assume A16: X is empty ; :: thesis: ex k being Element of NAT ex k being Element of NAT st X c= f . k
take k = 0 ; :: thesis: ex k being Element of NAT st X c= f . k
{} c= f . k by XBOOLE_1:2;
hence ex k being Element of NAT st X c= f . k by A16; :: thesis: verum

end;

hence ex k being Element of NAT st X c= f . k by A3; :: thesis: verum