let S1, S2 be ExtREAL_sequence; ( ( for n being Nat holds S1 . n = (H . n) . x ) & ( for n being Nat holds S2 . n = (H . n) . x ) implies S1 = S2 )
assume that
A2:
for n being Nat holds S1 . n = (H . n) . x
and
A3:
for n being Nat holds S2 . n = (H . n) . x
; S1 = S2
hence
S1 = S2
by FUNCT_2:63; verum