let seq, seq9 be Real_Sequence of N; :: thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) & ( for n being Element of NAT holds seq9 . n = (seq1 . n) + (seq2 . n) ) implies seq = seq9 )
assume that
A1: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) and
A2: for n being Element of NAT holds seq9 . n = (seq1 . n) + (seq2 . n) ; :: thesis: seq = seq9

now

let n be Element of NAT ; :: thesis: seq . n = seq9 . n
seq . n = (seq1 . n) + (seq2 . n) by A1;
hence seq . n = seq9 . n by A2; :: thesis: verum

end;

hence seq = seq9 by FUNCT_2:113; :: thesis: verum