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