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