deffunc H_{1}( Element of bool X) -> Element of ExtREAL = inf (Svc (M,$1));

thus ex G being Function of (bool X),ExtREAL st

for A being Subset of X holds G . A = H_{1}(A)
from FUNCT_2:sch 4(); :: thesis: verum

thus ex G being Function of (bool X),ExtREAL st

for A being Subset of X holds G . A = H