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
A1: for n being Nat holds H1 . n = (H . n) ^ and
A2: for n being Nat holds H2 . n = (H . n) ^ ; :: thesis: H1 = H2

now

let n be Element of NAT ; :: thesis: H1 . n = H2 . n
( H1 . n = (H . n) ^ & H2 . n = (H . n) ^ ) by A1, A2;
hence H1 . n = H2 . n ; :: thesis: verum

end;

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