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:113
.= 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