let X be non empty set ; :: thesis: 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 ; :: thesis: 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); :: thesis: 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; :: thesis: for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i)
let B be Element of Fin X; :: thesis: 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 ;
:: thesis: verum