let n be Nat; :: thesis: for A being non empty finite Subset of NAT
for f being Function of n,A st ex m being Nat st succ m = n & rng f = A & ( for n, m being Nat st m in dom f & n in dom f & n < m holds
f . n in f . m ) holds
f . () = union (rng f)

let A be non empty finite Subset of NAT; :: thesis: for f being Function of n,A st ex m being Nat st succ m = n & rng f = A & ( for n, m being Nat st m in dom f & n in dom f & n < m holds
f . n in f . m ) holds
f . () = union (rng f)

let f be Function of n,A; :: thesis: ( ex m being Nat st succ m = n & rng f = A & ( for n, m being Nat st m in dom f & n in dom f & n < m holds
f . n in f . m ) implies f . () = union (rng f) )

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: f . () = union (rng f)
thus f . () c= union (rng f) :: according to XBOOLE_0:def 10 :: thesis: union (rng f) c= f . ()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f . () or a in union (rng f) )
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 ;
assume a in f . () ; :: thesis: a in union (rng f)
then a in f . m by ;
hence a in union (rng f) by ; :: thesis: verum
end;
thus union (rng f) c= f . () :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union (rng f) or a in f . () )
assume a in union (rng f) ; :: thesis: a in f . ()
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 ;
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 ;
consider m being Nat such that
A11: n = succ m by A1;
i c= m by ;
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 ;
A15: now :: thesis: ( f . i in f . m implies a in f . () )
i in dom f by ;
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 ;
then reconsider i2 = f . m as Nat by A2;
assume f . i in f . m ; :: thesis: a in f . ()
then i1 c= i2 by ORDINAL1:def 2;
then a in i2 by A6, A9;
hence a in f . () by ; :: thesis: verum
end;
( i in { k where k is Nat : k < m } or i = m ) by ;
then ( ex k being Nat st
( k = i & k < m ) or i = m ) ;
hence a in f . () by A3, A6, A8, A9, A11, A14, A15, ORDINAL2:2; :: thesis: verum
end;