let v be VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,l_add ,l_mult #); :: thesis: 1 * v = v
1 * v = 1 (#) (seq_id v) by Th5
.= seq_id v by SEQ_1:35 ;
hence 1 * v = v by Def2; :: thesis: verum