let n be Element of 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 Element of NAT st succ m = n and
A2: rng f = A and
A3: for n, m being Element of 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:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
consider m being Element of 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:

proof

let a be set ; :: 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 set such that
A8: c in dom f and
A9: f . c = b by A7, FUNCT_1:def 3;
reconsider i = c as Ordinal by A8;
reconsider i = i as Element of NAT by A8, ORDINAL1:10;
consider m being Element of NAT such that
A10: n = succ m by A1;
i c= m by A8, A10, ORDINAL1:22;
then ( i c< m or i = m ) by XBOOLE_0:def 8;
then A11: ( i in m or i = m ) by ORDINAL1:11;
A12: dom f = n by FUNCT_2:def 1;
then A13: m in dom f by A10, ORDINAL1:6;

A14: now

i in dom f by A11, A12, A13, ORDINAL1:10;
then f . i in rng f by FUNCT_1:3;
then reconsider i1 = f . i as Element of NAT by A2;
f . m in rng f by A10, A12, FUNCT_1:3, ORDINAL1:6;
then reconsider i2 = f . m as Element of 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 A10, ORDINAL2:2; :: thesis:

end;

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

end;