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 holds FinUnion {.i.},f = f . i
let A be set ; :: thesis: for f being Function of X,(Fin A)
for i being Element of X holds FinUnion {.i.},f = f . i
let f be Function of X,(Fin A); :: thesis: for i being Element of X holds FinUnion {.i.},f = f . i
let i be Element of X; :: thesis: FinUnion {.i.},f = f . i
FinUnion A is commutative by Th50;
hence FinUnion {.i.},f = f . i by Th26, Th51; :: thesis: verum