let H1, H2 be Functional_Sequence of X,ExtREAL; :: thesis: ( ( for n being Nat holds H1 . n = r (#) (F . n) ) & ( for n being Nat holds H2 . n = r (#) (F . n) ) implies H1 = H2 )

assume that

A1: for n being Nat holds H1 . n = r (#) (F . n) and

A2: for n being Nat holds H2 . n = r (#) (F . n) ; :: thesis: H1 = H2

assume that

A1: for n being Nat holds H1 . n = r (#) (F . n) and

A2: for n being Nat holds H2 . n = r (#) (F . n) ; :: thesis: H1 = H2

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

hence
H1 = H2
by FUNCT_2:63; :: thesis: verumlet n be Element of NAT ; :: thesis: H1 . n = H2 . n

H1 . n = r (#) (F . n) by A1;

hence H1 . n = H2 . n by A2; :: thesis: verum

end;H1 . n = r (#) (F . n) by A1;

hence H1 . n = H2 . n by A2; :: thesis: verum