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 H₁( 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 = H₁(a) ) ) from FUNCT_1:sch 3();
reconsider A = rng g as finite set by A4, FINSET_1:8;

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: b in NAT
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 A5, FUNCT_1:3, TARSKI:def 3;
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 A2, TARSKI:def 4;
consider d being object such that
A10: d in dom f and
A11: f . d = c by A9, FUNCT_1:def 3;
reconsider d = d as Nat by A10;
d in { i where i is Nat : b in f . i } by A8, A11;
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: a in NAT
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 A12, NAT_1:def 1;
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 A4, A7, FUNCT_1:3;
hence b in f . a by A13, A15, Th2; :: 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