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: ex w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) st v + w = 0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #)
reconsider w = - (seq_id v) as VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) by Def1;
for s being Element of NAT holds ((seq_id v) + (- (seq_id v))) . s = (seq_id CZeroseq) . s

proof

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

end;

then A1: (seq_id v) + (- (seq_id v)) = seq_id CZeroseq by FUNCT_2:63
.= CZeroseq by Def2 ;
v + w = (seq_id v) + (seq_id w) by Def4
.= (seq_id v) + (- (seq_id v)) by Th3 ;
hence ex w being VECTOR of CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) st v + w = 0. CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) by A1; :: thesis: verum