let p, q be Element of (Formal-Series (n,L)); :: according to RLVECT_1:def 2 :: 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