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 * v) + (z2 * v)
let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: thesis: (z1 + z2) * v = (z1 * v) + (z2 * v)
for s being Element of NAT holds ((z1 + z2) (#) (seq_id v)) . s = ((z1 (#) (seq_id v)) + (z2 (#) (seq_id v))) . s

proof

let s be Element of NAT ; :: thesis: ((z1 + z2) (#) (seq_id v)) . s = ((z1 (#) (seq_id v)) + (z2 (#) (seq_id v))) . s
((z1 + z2) (#) (seq_id v)) . s = (z1 + z2) * ((seq_id v) . s) by VALUED_1:6
.= (z1 * ((seq_id v) . s)) + (z2 * ((seq_id v) . s))
.= ((z1 (#) (seq_id v)) . s) + (z2 * ((seq_id v) . s)) by VALUED_1:6
.= ((z1 (#) (seq_id v)) . s) + ((z2 (#) (seq_id v)) . s) by VALUED_1:6 ;
hence ((z1 + z2) (#) (seq_id v)) . s = ((z1 (#) (seq_id v)) + (z2 (#) (seq_id v))) . s by VALUED_1:1; :: thesis: verum

end;

then A1: (z1 + z2) (#) (seq_id v) = (z1 (#) (seq_id v)) + (z2 (#) (seq_id v)) by FUNCT_2:63;
(z1 * v) + (z2 * v) = (seq_id (z1 * v)) + (seq_id (z2 * v)) by Def4
.= (seq_id (z1 (#) (seq_id v))) + (seq_id (z2 * v)) by Th5
.= (seq_id (z1 (#) (seq_id v))) + (seq_id (z2 (#) (seq_id v))) by Th5
.= (z1 (#) (seq_id v)) + (seq_id (z2 (#) (seq_id v))) by Th3
.= (z1 (#) (seq_id v)) + (z2 (#) (seq_id v)) by Th3 ;
hence (z1 + z2) * v = (z1 * v) + (z2 * v) by A1, Th5; :: thesis: verum