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