set X = (dom f1) /\ (dom f2);
thus for F, G being PartFunc of C,ExtREAL 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 SEQ_1:sch 4(); :: thesis: verum