let A be set ; :: thesis: FinPairUnion A is commutative
let a, b be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def 2 :: 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