set V = CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #);
let v be VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #); :: thesis: v + (0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)) = v
A1: for s being Element of NAT holds ((seq_id v) + (seq_id CZeroseq)) . s = (seq_id v) . s

proof

let s be Element of NAT ; :: thesis: ((seq_id v) + (seq_id CZeroseq)) . s = (seq_id v) . s
((seq_id v) + (seq_id CZeroseq)) . s = ((seq_id v) . s) + ((seq_id CZeroseq) . s) by VALUED_1:1
.= ((seq_id v) . s) + 0c by Def6 ;
hence ((seq_id v) + (seq_id CZeroseq)) . s = (seq_id v) . s ; :: thesis: verum

end;

v + (0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)) = (seq_id v) + (seq_id CZeroseq) by Def4;
hence v + (0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)) = seq_id v by A1, FUNCT_2:63
.= v by Def2 ;
:: thesis: verum