let r be Real; :: thesis: for v being VECTOR of holds r * v = r (#) (seq_id v)
let v be VECTOR of ; :: 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