let X be non empty set ; :: thesis: for A being set
for f being Function of X,(Fin A)
for i, j, k being Element of X holds FinUnion {.i,j,k.},f = ((f . i) \/ (f . j)) \/ (f . k)
let A be set ; :: thesis: for f being Function of X,(Fin A)
for i, j, k being Element of X holds FinUnion {.i,j,k.},f = ((f . i) \/ (f . j)) \/ (f . k)
let f be Function of X,(Fin A); :: thesis: for i, j, k being Element of X holds FinUnion {.i,j,k.},f = ((f . i) \/ (f . j)) \/ (f . k)
let i, j, k be Element of X; :: thesis: FinUnion {.i,j,k.},f = ((f . i) \/ (f . j)) \/ (f . k)
( FinUnion A is idempotent & FinUnion A is commutative & FinUnion A is associative ) by Th49, Th50, Th51;
hence FinUnion {.i,j,k.},f = (FinUnion A) . ((FinUnion A) . (f . i),(f . j)),(f . k) by Th28
.= (FinUnion A) . ((f . i) \/ (f . j)),(f . k) by Def4
.= ((f . i) \/ (f . j)) \/ (f . k) by Def4 ;
:: thesis: verum