set X = dom f;
thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = H₁(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds
G . c = H₁(c) ) holds
F = G from SEQ_1:sch 4(); :: thesis: verum