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 ) by Th34, Th35;
hence FinUnion ({.i,j,k.},f) = (FinUnion A) . (((FinUnion A) . ((f . i),(f . j))),(f . k)) by Th16, Th36
.= (FinUnion A) . (((f . i) \/ (f . j)),(f . k)) by Def4
.= ((f . i) \/ (f . j)) \/ (f . k) by Def4 ;
:: thesis: verum