let r be Real; :: thesis: for v being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds r * v = r (#) (seq_id v)
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); :: thesis: r * v = r (#) (seq_id v)
thus r * v = (R_id r) (#) (seq_id v) by Def5
.= r (#) (seq_id v) by Def3 ; :: thesis: verum