let A be non-empty with_catenation associative UAStr ; for I1, I2, I3 being Element of A holds (I1 \; I2) \; I3 = I1 \; (I2 \; I3)
let I1, I2, I3 be Element of A; (I1 \; I2) \; I3 = I1 \; (I2 \; I3)
reconsider f = the charact of A . 2 as non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of A *), the carrier of A by Def14;
A1:
2 in dom the charact of A
by Def11;
arity f = 2
by COMPUT_1:def 21;
then A2:
dom f = 2 -tuples_on the carrier of A
by COMPUT_1:22;
A3:
In (2,(dom the charact of A)) = 2
by A1, SUBSET_1:def 8;
A4:
<*I1,I2*> in dom f
by A2, FINSEQ_2:137;
A5:
<*I2,I3*> in dom f
by A2, FINSEQ_2:137;
A6:
<*I1,(I2 \; I3)*> in dom f
by A2, FINSEQ_2:137;
<*(I1 \; I2),I3*> in dom f
by A2, FINSEQ_2:137;
hence
(I1 \; I2) \; I3 = I1 \; (I2 \; I3)
by A3, A4, A5, A6, Def2; verum