set X = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty})));
thus for f, g being PartFunc of C,ExtREAL st dom f = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom f holds
f . c = H₁(c) ) & dom g = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( 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