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 Def11;
thus v * w = q *' p by Def11
.= w * v by Def11 ; :: thesis: verum