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