let H1, H2 be Functional_Sequence of D,REAL; :: thesis: ( ( for n being Nat holds H1 . n = ||.(H . n).|| ) & ( for n being Nat holds H2 . n = ||.(H . n).|| ) implies H1 = H2 )
assume that
A6: for n being Nat holds H1 . n = ||.(H . n).|| and
A7: for n being Nat holds H2 . n = ||.(H . n).|| ; :: thesis: H1 = H2

now :: thesis: for n being Element of NAT holds H1 . n = H2 . n

let n be Element of NAT ; :: thesis: H1 . n = H2 . n
H2 . n = ||.(H . n).|| by A7;
hence H1 . n = H2 . n by A6; :: thesis: verum

end;

hence H1 = H2 by FUNCT_2:63; :: thesis: verum