defpred S1[ 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
A7: for c being Element of C holds
( c in dom F iff S1[c] ) and
A8: for c being Element of C st c in dom F holds
F . c = H2(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) ) )
for x being object st x in dom F holds
x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty})))
proof
let x be object ; :: thesis: ( x in dom F implies x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) )
assume A9: x in dom F ; :: thesis: x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty})))
dom F c= C by RELAT_1:def 18;
then reconsider x = x as Element of C by A9;
x in dom F by A9;
hence x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by A7; :: thesis: verum
end;
then A10: dom F c= ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) ;
for x being object st x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) holds
x in dom F
proof
let x be object ; :: thesis: ( x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) implies x in dom F )
assume A11: x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) ; :: thesis: x in dom F
then A12: x in dom f1 by XBOOLE_0:def 4;
dom f1 c= C by RELAT_1:def 18;
then reconsider x = x as Element of C by A12;
x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by A11;
hence x in dom F by A7; :: thesis: verum
end;
then ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) c= dom F ;
hence dom F = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by A10, 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 c in dom F ; :: thesis: F . c = (f1 . c) - (f2 . c)
hence F . c = (f1 . c) - (f2 . c) by A8; :: thesis: verum