let v, w be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: according to RLVECT_1:def 2 :: thesis: v + w = w + v
v + w = (seq_id v) + (seq_id w) by Def4;
hence v + w = w + v by Def4; :: thesis: verum