set Pm = Polynom-Ring (n,L);
let v, w be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
reconsider p = v, q = w as Polynomial of n,L by Def11;
thus v + w = q + p by Def11
.= w + v by Def11 ; :: thesis: verum