let A be non-empty with_catenation associative UAStr ; :: thesis: for I1, I2, I3 being Element of A holds (I1 \; I2) \; I3 = I1 \; (I2 \; I3)
let I1, I2, I3 be Element of A; :: thesis: (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;
( 2 in dom the charact of A & arity f = 2 ) by Def11, COMPUT_1:def 26;
then ( dom f = 2 -tuples_on the carrier of A & In 2,(dom the charact of A) = 2 ) by COMPUT_1:25, FUNCT_7:def 1;
then ( I1 \; I2 = f . <*I1,I2*> & I2 \; I3 = f . <*I2,I3*> & (I1 \; I2) \; I3 = f . <*(I1 \; I2),I3*> & I1 \; (I2 \; I3) = f . <*I1,(I2 \; I3)*> & <*I1,I2*> in dom f & <*I2,I3*> in dom f & <*I1,(I2 \; I3)*> in dom f & <*(I1 \; I2),I3*> in dom f ) by CATALG_1:10;
hence (I1 \; I2) \; I3 = I1 \; (I2 \; I3) by Def2; :: thesis: verum