let X be non empty set ; for A being set
for f being Function of X,(Fin A)
for i being Element of X
for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)
let A be set ; for f being Function of X,(Fin A)
for i being Element of X
for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)
let f be Function of X,(Fin A); for i being Element of X
for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)
let i be Element of X; for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)
let B be Element of Fin X; FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)
A1:
FinUnion A is associative
by Th36;
( FinUnion A is idempotent & FinUnion A is commutative )
by Th34, Th35;
hence FinUnion ((B \/ {.i.}),f) =
(FinUnion A) . ((FinUnion (B,f)),(f . i))
by A1, Th29, Th38
.=
(FinUnion (B,f)) \/ (f . i)
by Def4
;
verum