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