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