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

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_{1}( 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_{1}(a) ) )
from FUNCT_1:sch 3();

reconsider A = rng g as finite set by A4, FINSET_1:8;

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

end;consider g being Function such that

A4: ( dom g = X & ( for a being object st a in X holds

g . a = H

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

assume
not X is empty
; :: thesis: ex a being Nat st X c= f . ab 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 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

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 ;

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;

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

end;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

then reconsider Y = Y as non empty Subset of NAT by TARSKI:def 3;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;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

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 )

Y9 in A
by A4, A7, FUNCT_1:3;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;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

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

now :: thesis: ( X is empty implies ex k being Element of omega ex k being Nat st X c= f . k )

hence
ex k being Nat st X c= f . k
by A3; :: thesis: verumassume 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;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