deffunc H_{1}( 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_{1}(z) ) & dom g = dom f & ( for z being Element of X st z in dom g holds

g . z = H_{1}(z) ) holds

h = g from SEQ_1:sch 4(); :: thesis: verum

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

g . z = H

h = g from SEQ_1:sch 4(); :: thesis: verum