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 binary 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 26;
then A2:
dom f = 2 -tuples_on the carrier of A
by COMPUT_1:25;
A3:
In 2,(dom the charact of A) = 2
by A1, FUNCT_7:def 1;
A4:
<*I1,I2*> in dom f
by A2, FINSEQ_2:157;
A5:
<*I2,I3*> in dom f
by A2, FINSEQ_2:157;
A6:
<*I1,(I2 \; I3)*> in dom f
by A2, FINSEQ_2:157;
<*(I1 \; I2),I3*> in dom f
by A2, FINSEQ_2:157;
hence
(I1 \; I2) \; I3 = I1 \; (I2 \; I3)
by A3, A4, A5, A6, Def2; verum