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

reconsider p1 = p, q1 = q as sequence of L by Def2;

thus p * q = p1 *' q1 by Def2

.= q * p by Def2 ; :: thesis: verum