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