deffunc H₁( Element of MapsT X) -> Element of TOL X = cod $1;
thus ex f being Function of (MapsT X),(TOL X) st
for x being Element of MapsT X holds f . x = H₁(x) from FUNCT_2:sch 4(); :: thesis: verum