deffunc H₁( Element of NAT ) -> Element of the carrier of L = (p . $1) / (p . ((len p) -' 1));
consider q being sequence of L such that
A1: for n being Element of NAT holds q . n = H₁(n) from FUNCT_2:sch 4();
take q ; :: thesis: for n being Element of NAT holds q . n = (p . n) / (p . ((len p) -' 1))
thus for n being Element of NAT holds q . n = (p . n) / (p . ((len p) -' 1)) by A1; :: thesis: verum