let A be set ; :: thesis: FinUnion A is commutative
let x be Element of Fin A; :: according to BINOP_1:def 13 :: 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