thus for h, g being PartFunc of , st dom h = dom f & ( for x being Element of X st x in dom h holds
h . x = H₁(x) ) & dom g = dom f & ( for x being Element of X st x in dom g holds
g . x = H₁(x) ) holds
h = g from SEQ_1:sch 4(); :: thesis: verum