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: v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = v
A1: for s being set st s in NAT holds
((seq_id v) + (seq_id Zeroseq)) . s = (seq_id v) . s

proof

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

end;

v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = (seq_id v) + (seq_id Zeroseq) by Def4;
hence v + (0. RLSStruct(# the_set_of_RealSequences,Zeroseq,l_add,l_mult #)) = seq_id v by A1, FUNCT_2:12
.= v by Def2 ;
:: thesis: verum