deffunc H₁( Element of NAT ) -> Element of the carrier of X = (1r / ($1 !c)) * (z #N $1);
thus ex s being sequence of X st
for n being Element of NAT holds s . n = H₁(n) from FUNCT_2:sch 4(); :: thesis: verum