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 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 ) & X c= union (rng f) ) ; :: thesis: ex k being Element of NAT st X c= f . k

A2: now

assume A3: 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 A3; :: thesis: verum

end;

now

assume A4: not X is empty ; :: thesis: ex a being Element of NAT st X c= f . a
deffunc H₁( set ) -> Element of NAT = min* { i where i is Element of NAT : $1 in f . i } ;
consider g being Function such that
A5: ( 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 A5, FINSET_1:26;

A6: 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
A7: ( 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 A5, A7;
hence b in NAT ; :: thesis: verum

end;

consider c being set such that
A8: c in dom g by A4, A5, XBOOLE_0:def 1;
reconsider A = A as non empty finite Subset of NAT by A6, A8, 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 A9: b in X ; :: thesis: b in f . a
then consider c being set such that
A10: ( b in c & c in rng f ) by A1, TARSKI:def 4;
consider d being set such that
A11: ( d in dom f & f . d = c ) by A10, FUNCT_1:def 5;
reconsider d = d as Element of NAT by A11;
d in { i where i is Element of NAT : b in f . i } by A10, 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 consider i being Element of NAT such that
A12: ( i = a & b in f . i ) ;
thus a in NAT by A12; :: thesis: verum

end;

then reconsider Y = Y as non empty Subset of NAT by TARSKI:def 3;
A13: g . b = min* Y by A5, A9;
then reconsider Y' = g . b as Element of NAT ;
( Y' in Y & ( for k being Element of NAT st k in Y holds
Y' <= k ) ) by A13, NAT_1:def 1;
then consider i being Element of NAT such that
A14: ( i = g . b & b in f . i ) ;
A15: Y' in A by A5, A9, FUNCT_1:12;
A16: dom f = NAT by FUNCT_2:def 1;

now

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

end;

hence b in f . a by A14, A15, Th2; :: thesis: verum

end;

end;

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