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