let A be set ; FinPairUnion A is associative
let a, b, c be Element of [:(Fin A),(Fin A):]; BINOP_1:def 3 (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 Th3
.=
((FinPairUnion A) . (a,b)) \/ c
by Def6
.=
(FinPairUnion A) . (((FinPairUnion A) . (a,b)),c)
by Def6
; verum