defpred S₁[ Element of NAT , Element of ExtREAL ] means ( ( $1 in S implies $2 = H . $1 ) & ( not $1 in S implies $2 = 0. ) );
A1: for n being Element of NAT ex y being Element of ExtREAL st S₁[n,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of ExtREAL st S₁[n,y]

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

suppose n in S ; :: thesis: ex y being Element of ExtREAL st S₁[n,y]

then reconsider n = n as Element of S ;
take H . n ; :: thesis: S₁[n,H . n]
thus S₁[n,H . n] ; :: thesis: verum

end;

suppose A2: not n in S ; :: thesis: ex y being Element of ExtREAL st S₁[n,y]

take 0. ; :: thesis: S₁[n, 0. ]
thus S₁[n, 0. ] by A2; :: thesis: verum

end;

end;

end;

consider GG being Function of NAT,ExtREAL such that
A3: for n being Element of NAT holds S₁[n,GG . n] from FUNCT_2:sch 3(A1);
take GG ; :: thesis: for n being Element of NAT holds
( ( n in S implies GG . n = H . n ) & ( not n in S implies GG . n = 0. ) )
thus for n being Element of NAT holds
( ( n in S implies GG . n = H . n ) & ( not n in S implies GG . n = 0. ) ) by A3; :: thesis: verum