let u, v, w be VECTOR of RLSStruct(# the_set_of_RealSequences ,Zeroseq ,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 SEQ_1:20
.= (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