let z be Complex; :: thesis: for v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) holds z * (v + w) = (z * v) + (z * w)
let v, w be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: thesis: z * (v + w) = (z * v) + (z * w)
A1: z * (v + w) = z (#) (seq_id (v + w)) by Th5
.= z (#) (seq_id ((seq_id v) + (seq_id w))) by Def4
.= z (#) ((seq_id v) + (seq_id w)) by Th3
.= (z (#) (seq_id v)) + (z (#) (seq_id w)) by COMSEQ_1:16 ;
(z * v) + (z * w) = (seq_id (z * v)) + (seq_id (z * w)) by Def4
.= (seq_id (z (#) (seq_id v))) + (seq_id (z * w)) by Th5
.= (seq_id (z (#) (seq_id v))) + (seq_id (z (#) (seq_id w))) by Th5
.= (z (#) (seq_id v)) + (seq_id (z (#) (seq_id w))) by Th3
.= (z (#) (seq_id v)) + (z (#) (seq_id w)) by Th3 ;
hence z * (v + w) = (z * v) + (z * w) by A1; :: thesis: verum