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 n) = 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 n) = 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 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 ; :: thesis: f . (union n) = union (rng f)

thus f . (union n) c= union (rng f) :: according to XBOOLE_0:def 10 :: thesis: union (rng f) c= f . (union n)

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; :: 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 n) = 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 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 ; :: thesis: f . (union n) = union (rng f)

thus f . (union n) c= union (rng f) :: according to XBOOLE_0:def 10 :: thesis: union (rng f) c= f . (union n)

proof

thus
union (rng f) c= f . (union n)
:: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f . (union n) 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 A4, FUNCT_1:3, ORDINAL1:6;

assume a in f . (union n) ; :: thesis: a in union (rng f)

then a in f . m by A4, ORDINAL2:2;

hence a in union (rng f) by A5, TARSKI:def 4; :: thesis: verum

end;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: a in union (rng f)

then a in f . m by A4, ORDINAL2:2;

hence a in union (rng f) by A5, TARSKI:def 4; :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union (rng f) or a in f . (union n) )

assume a in union (rng f) ; :: thesis: 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;

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: verum

end;assume a in union (rng f) ; :: thesis: 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;

A15: now :: thesis: ( f . i in f . m implies a in f . (union n) )

( i in { k where k is Nat : k < m } or i = m )
by A12, AXIOMS:4;
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: a in f . (union n)

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: verum

end;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: a in f . (union n)

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: verum

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: verum