let u, v, w be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: thesis: (u + v) + w = u + (v + w)
(u + v) + w = (seq_id (u + v)) + (seq_id w) by Def4
.= (seq_id ((seq_id u) + (seq_id v))) + (seq_id w) by Def4
.= ((seq_id u) + (seq_id v)) + (seq_id w) by Th3
.= (seq_id u) + ((seq_id v) + (seq_id w)) by COMSEQ_1:7
.= (seq_id u) + (seq_id ((seq_id v) + (seq_id w))) by Th3
.= (seq_id u) + (seq_id (v + w)) by Def4 ;
hence (u + v) + w = u + (v + w) by Def4; :: thesis: verum