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