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