let C be non empty set ; :: thesis:
let f be sequence of C; :: thesis:
let X be finite set ; :: thesis:
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:

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;

let b be object ; :: thesis:
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:

end;

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: b in X ; :: thesis:
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 ;

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;

assume Y9 in a ; :: thesis:
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:

end;

end;

end;