set Pm = Polynom-Ring (n,L);
let v, w be Element of (Polynom-Ring (n,L)); :: according to GROUP_1:def 12 :: thesis: v * w = w * v
reconsider p = v, q = w as Polynomial of n,L by Def27;
thus v * w = q *' p by Def27
.= w * v by Def27 ; :: thesis: verum