set X = (dom f) \ (f " {0. });
thus for F, G being PartFunc of C,ExtREAL 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 SEQ_1:sch 4(); :: thesis: verum