set V = RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #);
let v be VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #); :: thesis: ex w being VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)
reconsider w = - (seq_id v) as VECTOR of RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) by Def1;
for s being set st s in NAT holds
((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s

proof

let s be set ; :: thesis: ( s in NAT implies ((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s )
assume A1: s in NAT ; :: thesis: ((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s
((seq_id v) + (- (seq_id v))) . s = ((seq_id v) . s) + ((- (seq_id v)) . s) by A1, SEQ_1:7
.= ((seq_id v) . s) + (- ((seq_id v) . s)) by A1, SEQ_1:10
.= (seq_id Zeroseq) . s by A1, Def6 ;
hence ((seq_id v) + (- (seq_id v))) . s = (seq_id Zeroseq) . s ; :: thesis: verum

end;

then A2: (seq_id v) + (- (seq_id v)) = seq_id Zeroseq by FUNCT_2:12
.= Zeroseq 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 RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #) by A2; :: thesis: verum