let A be set ; :: thesis: FinPairUnion A is idempotent
let a be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def 4 :: thesis: (FinPairUnion A) . (a,a) = a
thus (FinPairUnion A) . (a,a) = a \/ a by Def6
.= a ; :: thesis: verum