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 Th51;
( FinUnion A is idempotent & FinUnion A is commutative ) by Th49, Th50;
hence FinUnion (B \/ {.i.}),f = (FinUnion A) . (FinUnion B,f),(f . i) by A1, Th41, Th53
.= (FinUnion B,f) \/ (f . i) by Def4 ;
:: thesis: verum