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