set Pm = Polynom-Ring n,L;
let v, w be Element of (Polynom-Ring n,L); :: according to GROUP_1:def 16 :: 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