thus for f, g being PartFunc of X,the carrier of V st dom f = dom f & ( for x being Element of X st x in dom f holds
f /. x = H₂(x) ) & dom g = dom f & ( for x being Element of X st x in dom g holds
g /. x = H₂(x) ) holds
f = g from PARTFUN2:sch 3(); :: thesis: verum