let z1, z2 be Complex; :: thesis: for v being VECTOR of holds (z1 * z2) * v = z1 * (z2 * v)
let v be VECTOR of ; :: 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:20
.= 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