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 Th35;
hence FinUnion ({.i.},f) = f . i by Th14, Th36; :: thesis: verum