defpred S₁[ Element of C] means $1 in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty })));
consider F being PartFunc of C,ExtREAL such that
A15: for c being Element of C holds
( c in dom F iff S₁[c] ) and
A16: for c being Element of C st c in dom F holds
F . c = H₂(c) from SEQ_1:sch 3();
take F ; :: thesis: ( 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 = (f1 . c) - (f2 . c) ) )
A17: for x being set st x in dom F holds
x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty })))

proof

let x be set ; :: thesis: ( x in dom F implies x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) )
assume A18: x in dom F ; :: thesis: x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty })))
A19: dom F c= C by RELAT_1:def 18;
reconsider x = x as Element of C by A18, A19;
A20: x in dom F by A18;
thus x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) by A15, A20; :: thesis: verum

end;

A21: dom F c= ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) by A17, TARSKI:def 3;
A22: for x being set st x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) holds
x in dom F

proof

let x be set ; :: thesis: ( x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) implies x in dom F )
assume A23: x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) ; :: thesis: x in dom F
A24: x in dom f1 by A23, XBOOLE_0:def 4;
A25: dom f1 c= C by RELAT_1:def 18;
reconsider x = x as Element of C by A24, A25;
A26: x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) by A23;
thus x in dom F by A15, A26; :: thesis: verum

end;

A27: ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) c= dom F by A22, TARSKI:def 3;
thus dom F = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) by A21, A27, XBOOLE_0:def 10; :: thesis: for c being Element of C st c in dom F holds
F . c = (f1 . c) - (f2 . c)
let c be Element of C; :: thesis: ( c in dom F implies F . c = (f1 . c) - (f2 . c) )
assume A28: c in dom F ; :: thesis: F . c = (f1 . c) - (f2 . c)
thus F . c = (f1 . c) - (f2 . c) by A16, A28; :: thesis: verum