let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: thesis: 1r * v = v
1r * v = 1r (#) (seq_id v) by Th5
.= seq_id v by COMSEQ_1:21 ;
hence 1r * v = v by Def2; :: thesis: verum