let A be set ; :: thesis: FinPairUnion A is associative
let a, b, c be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def 14 :: thesis: (FinPairUnion A) . a,((FinPairUnion A) . b,c) = (FinPairUnion A) . ((FinPairUnion A) . a,b),c
thus (FinPairUnion A) . a,((FinPairUnion A) . b,c) = a \/ ((FinPairUnion A) . b,c) by Def6
.= a \/ (b \/ c) by Def6
.= (a \/ b) \/ c by Th16
.= ((FinPairUnion A) . a,b) \/ c by Def6
.= (FinPairUnion A) . ((FinPairUnion A) . a,b),c by Def6 ; :: thesis: verum