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

proof

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

end;

hence seq1 = seq2 by FUNCT_2:113; :: thesis: verum