set Pm = Polynom-Ring n,L;
let x, y, z be Element of (Polynom-Ring n,L); :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
reconsider p = x, q = y, r = z as Polynomial of n,L by Def27;
A1: y * z = q *' r by Def27;
x * y = p *' q by Def27;
hence (x * y) * z = (p *' q) *' r by Def27
.= p *' (q *' r) by Th86
.= x * (y * z) by A1, Def27 ;
:: thesis: verum