for A being non-empty with_catenation associative UAStr
for I1, I2, I3 being Element of A holds (I1 \; I2) \; I3 = I1 \; (I2 \; I3)