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