let z be Complex; :: thesis: for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds z * v = z (#) (seq_id v)
let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #); :: 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