set X = (dom f) \ (f " {0.});
deffunc H₂( Element of C) -> Element of ExtREAL = r / (f . $1);
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