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