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