let v, w be VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #); :: according to RLVECT_1:def 5 :: thesis: v + w = w + v
v + w = (seq_id v) + (seq_id w) by Def4;
hence v + w = w + v by Def4; :: thesis: verum