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