set X = (dom f) \ (f " {0 });
thus for f, g being PartFunc of C,COMPLEX st dom f = (dom f) \ (f " {0 }) & ( for c being Element of C st c in dom f holds
f /. c = H₁(c) ) & dom g = (dom f) \ (f " {0 }) & ( for c being Element of C st c in dom g holds
g /. c = H₁(c) ) holds
f = g from PARTFUN2:sch 3(); :: thesis: verum