let n be Nat; :: thesis:
let A be non empty finite Subset of NAT; :: thesis:
let f be Function of n,A; :: thesis:
assume that
A1: ex m being Nat st succ m = n and
A2: rng f = A and
A3: for n, m being Nat st m in dom f & n in dom f & n < m holds
f . n in f . m ; :: thesis:
thus f . (union n) c= union (rng f) :: according to XBOOLE_0:def 10 :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
consider m being Nat such that
A4: n = succ m by A1;
dom f = n by FUNCT_2:def 1;
then A5: f . m in rng f by A4, FUNCT_1:3, ORDINAL1:6;
assume a in f . (union n) ; :: thesis:
then a in f . m by A4, ORDINAL2:2;
hence a in union (rng f) by A5, TARSKI:def 4; :: thesis:

end;

thus union (rng f) c= f . (union n) :: thesis:

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in union (rng f) ; :: thesis:
then consider b being set such that
A6: a in b and
A7: b in rng f by TARSKI:def 4;
consider c being object such that
A8: c in dom f and
A9: f . c = b by A7, FUNCT_1:def 3;
dom f = n by PARTFUN1:def 2;
then A10: dom f in NAT by ORDINAL1:def 12;
reconsider i = c as Ordinal by A8;
reconsider i = i as Element of NAT by A8, ORDINAL1:10, A10;
consider m being Nat such that
A11: n = succ m by A1;
i c= m by A8, A11, ORDINAL1:22;
then ( i c< m or i = m ) ;
then A12: ( i in m or i = m ) by ORDINAL1:11;
A13: dom f = n by FUNCT_2:def 1;
then A14: m in dom f by A11, ORDINAL1:6;

A15: now :: thesis:

i in dom f by A12, A13, A14, ORDINAL1:10;
then f . i in rng f by FUNCT_1:3;
then reconsider i1 = f . i as Nat by A2;
f . m in rng f by A11, A13, FUNCT_1:3, ORDINAL1:6;
then reconsider i2 = f . m as Nat by A2;
assume f . i in f . m ; :: thesis:
then i1 c= i2 by ORDINAL1:def 2;
then a in i2 by A6, A9;
hence a in f . (union n) by A11, ORDINAL2:2; :: thesis:

end;

( i in { k where k is Nat : k < m } or i = m ) by A12, AXIOMS:4;
then ( ex k being Nat st
( k = i & k < m ) or i = m ) ;
hence a in f . (union n) by A3, A6, A8, A9, A11, A14, A15, ORDINAL2:2; :: thesis:

end;