let A be set ; :: thesis: FinUnion A is idempotent
let x be Element of Fin A; :: according to BINOP_1:def 4 :: thesis: (FinUnion A) . (x,x) = x
thus (FinUnion A) . (x,x) = x \/ x by Def4
.= x ; :: thesis: verum