let z1, z2 be Complex; :: thesis: for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds (z1 * z2) * v = z1 * (z2 * v)
let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: thesis: (z1 * z2) * v = z1 * (z2 * v)
(z1 * z2) * v = (z1 * z2) (#) (seq_id v) by Th5
.= z1 (#) (z2 (#) (seq_id v)) by COMSEQ_1:17
.= z1 (#) (seq_id (z2 (#) (seq_id v))) by Th3
.= z1 (#) (seq_id (z2 * v)) by Th5 ;
hence (z1 * z2) * v = z1 * (z2 * v) by Th5; :: thesis: verum