let p, q be Element of (Polynom-Ring L); :: according to GROUP_1:def 12 :: thesis: p * q = q * p
reconsider p1 = p, q1 = q as sequence of L by Def10;
thus p * q = p1 *' q1 by Def10
.= q * p by Def10 ; :: thesis: verum