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