let G1, G2 be sequence of ExtREAL; :: thesis: ( ( for n being Element of NAT holds ( ( n in S implies G1 . n = H . n ) & ( not n in S implies G1 . n =0. ) ) ) & ( for n being Element of NAT holds ( ( n in S implies G2 . n = H . n ) & ( not n in S implies G2 . n =0. ) ) ) implies G1 = G2 ) assume that A4:
for n being Element of NAT holds ( ( n in S implies G1 . n = H . n ) & ( not n in S implies G1 . n =0. ) )
and A5:
for n being Element of NAT holds ( ( n in S implies G2 . n = H . n ) & ( not n in S implies G2 . n =0. ) )
; :: thesis: G1 = G2
for n being object st n inNAT holds G1 . n = G2 . n