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