thus for f, g being PartFunc of C,V st dom f = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom f holds
f /. c = H₁(c) ) & dom g = (dom f1) /\ (dom f2) & ( 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