let n be Nat; 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 n) = union (rng f)
let A be 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 n) = union (rng f)
let f be Function of n,A; ( 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 n) = 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
; f . (union n) = union (rng f)
thus
f . (union n) c= union (rng f)
XBOOLE_0:def 10 union (rng f) c= f . (union n)
thus
union (rng f) c= f . (union n)
verumproof
let a be
object ;
TARSKI:def 3 ( not a in union (rng f) or a in f . (union n) )
assume
a in union (rng f)
;
a in f . (union n)
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;
(
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;
verum
end;