let p, q, r be Element of (Formal-Series L); :: according to GROUP_1:def 3 :: thesis: (p * q) * r = p * (q * r)

reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

A1: q * r = q1 *' r1 by Def2;

p * q = p1 *' q1 by Def2;

hence (p * q) * r = (p1 *' q1) *' r1 by Def2

.= p1 *' (q1 *' r1) by POLYNOM3:33

.= p * (q * r) by A1, Def2 ;

:: thesis: verum

reconsider p1 = p, q1 = q, r1 = r as sequence of L by Def2;

A1: q * r = q1 *' r1 by Def2;

p * q = p1 *' q1 by Def2;

hence (p * q) * r = (p1 *' q1) *' r1 by Def2

.= p1 *' (q1 *' r1) by POLYNOM3:33

.= p * (q * r) by A1, Def2 ;

:: thesis: verum