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