let z be Complex; :: thesis: for v being VECTOR of holds z * v = z (#) (seq_id v)
let v be VECTOR of ; :: thesis: z * v = z (#) (seq_id v)
thus z * v = l_mult . z,v
.= (C_id z) (#) (seq_id v) by Def5
.= z (#) (seq_id v) by Def3 ; :: thesis: verum