thus ex f being Function of X,T st
for x being Element of X holds f . x = H₁(x) from FUNCT_2:sch 4(); :: thesis: verum