let A be set ; :: thesis: FinUnion A is commutative
let x be Element of Fin A; :: according to BINOP_1:def 2 :: thesis: for b₁ being Element of Fin A holds (FinUnion A) . (x,b₁) = (FinUnion A) . (b₁,x)
let y be Element of Fin A; :: thesis: (FinUnion A) . (x,y) = (FinUnion A) . (y,x)
thus (FinUnion A) . (x,y) = y \/ x by Def4
.= (FinUnion A) . (y,x) by Def4 ; :: thesis: verum