let p, q, r be Element of (Formal-Series L); :: according to RLVECT_1:def 3 :: thesis: (p + q) + r = p + (q + r)

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

A1: q + r = q1 + r1 by Def2;

p + q = p1 + q1 by Def2;

hence (p + q) + r = (p1 + q1) + r1 by Def2

.= p1 + (q1 + r1) by POLYNOM3:26

.= p + (q + r) by A1, Def2 ;

:: thesis: verum

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

A1: q + r = q1 + r1 by Def2;

p + q = p1 + q1 by Def2;

hence (p + q) + r = (p1 + q1) + r1 by Def2

.= p1 + (q1 + r1) by POLYNOM3:26

.= p + (q + r) by A1, Def2 ;

:: thesis: verum