let p, q be Element of (Polynom-Ring L); :: according to RLVECT_1:def 2 :: thesis: p + q = q + p

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

thus p + q = p1 + q1 by Def10

.= q + p by Def10 ; :: thesis: verum

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

thus p + q = p1 + q1 by Def10

.= q + p by Def10 ; :: thesis: verum