let S1, S2 be Real_Sequence; ( ( for n being Nat holds S1 . n = (S . n) - x ) & ( for n being Nat holds S2 . n = (S . n) - x ) implies S1 = S2 )
assume that
A2:
for n being Nat holds S1 . n = (S . n) - x
and
A3:
for n being Nat holds S2 . n = (S . n) - x
; S1 = S2
for n being Nat holds S1 . n = S2 . n
hence
S1 = S2
; verum