set X = (dom f1) /\ ((dom f2) \ (f2 " {0 }));
thus for f, g being PartFunc of C,COMPLEX st dom f = (dom f1) /\ ((dom f2) \ (f2 " {0 })) & ( for c being Element of C st c in dom f holds
f /. c = H₁(c) ) & dom g = (dom f1) /\ ((dom f2) \ (f2 " {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