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