deffunc H₁( set ) -> object = (f . $1) to_power k;
thus for h, g being PartFunc of X,REAL st dom h = dom f & ( for z being Element of X st z in dom h holds
h . z = H₁(z) ) & dom g = dom f & ( for z being Element of X st z in dom g holds
g . z = H₁(z) ) holds
h = g from SEQ_1:sch 4(); :: thesis: verum