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 in NAT holds
G1 . n = G2 . n

proof

let n be object ; :: thesis: ( n in NAT implies G1 . n = G2 . n )
assume n in NAT ; :: thesis: G1 . n = G2 . n
then reconsider n = n as Element of NAT ;

per cases ( n in S or not n in S ) ;

suppose A6: n in S ; :: thesis: G1 . n = G2 . n

then G1 . n = H . n by A4;
hence G1 . n = G2 . n by A5, A6; :: thesis: verum

end;

suppose A7: not n in S ; :: thesis: G1 . n = G2 . n

then G1 . n = 0. by A4;
hence G1 . n = G2 . n by A5, A7; :: thesis: verum

end;

end;

end;

hence G1 = G2 by FUNCT_2:12; :: thesis: verum