defpred S₁[ Element of C] means $1 in (dom f1) /\ (dom f2);
consider F being PartFunc of C,ExtREAL such that
A29: for c being Element of C holds
( c in dom F iff S₁[c] ) and
A30: 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) & ( for c being Element of C st c in dom F holds
F . c = (f1 . c) * (f2 . c) ) )
A31: for x being set st x in dom F holds
x in (dom f1) /\ (dom f2)

proof

let x be set ; :: thesis: ( x in dom F implies x in (dom f1) /\ (dom f2) )
assume A32: x in dom F ; :: thesis: x in (dom f1) /\ (dom f2)
A33: dom F c= C by RELAT_1:def 18;
reconsider x = x as Element of C by A32, A33;
A34: x in dom F by A32;
thus x in (dom f1) /\ (dom f2) by A29, A34; :: thesis: verum

end;

A35: dom F c= (dom f1) /\ (dom f2) by A31, TARSKI:def 3;
A36: for x being set st x in (dom f1) /\ (dom f2) holds
x in dom F

proof

let x be set ; :: thesis: ( x in (dom f1) /\ (dom f2) implies x in dom F )
assume A37: x in (dom f1) /\ (dom f2) ; :: thesis: x in dom F
A38: x in dom f1 by A37, XBOOLE_0:def 4;
A39: dom f1 c= C by RELAT_1:def 18;
reconsider x = x as Element of C by A38, A39;
A40: x in (dom f1) /\ (dom f2) by A37;
thus x in dom F by A29, A40; :: thesis: verum

end;

A41: (dom f1) /\ (dom f2) c= dom F by A36, TARSKI:def 3;
thus dom F = (dom f1) /\ (dom f2) by A35, A41, 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 A42: c in dom F ; :: thesis: F . c = (f1 . c) * (f2 . c)
thus F . c = (f1 . c) * (f2 . c) by A30, A42; :: thesis: verum