thus for f1, g1 being PartFunc of Z,(REAL n) st dom f1 = dom f & ( for c being Element of Z st c in dom f1 holds
f1 /. c = H₁(c) ) & dom g1 = dom f & ( for c being Element of Z st c in dom g1 holds
g1 /. c = H₁(c) ) holds
f1 = g1 from PARTFUN2:sch 3(); :: thesis: verum