defpred S₁[ Element of C] means $1 in (dom f) \ (f " {0. });
consider F being PartFunc of C,ExtREAL such that
A1: for c being Element of C holds
( c in dom F iff S₁[c] ) and
A2: 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 f) \ (f " {0. }) & ( for c being Element of C st c in dom F holds
F . c = (R_EAL r) / (f . c) ) )
A3: for x being set st x in dom F holds
x in (dom f) \ (f " {0. })

proof

let x be set ; :: thesis: ( x in dom F implies x in (dom f) \ (f " {0. }) )
assume A4: x in dom F ; :: thesis: x in (dom f) \ (f " {0. })
A5: dom F c= C by RELAT_1:def 18;
reconsider x = x as Element of C by A4, A5;
A6: x in dom F by A4;
thus x in (dom f) \ (f " {0. }) by A1, A6; :: thesis: verum

end;

A7: dom F c= (dom f) \ (f " {0. }) by A3, TARSKI:def 3;
A8: for x being set st x in (dom f) \ (f " {0. }) holds
x in dom F

proof

let x be set ; :: thesis: ( x in (dom f) \ (f " {0. }) implies x in dom F )
assume A9: x in (dom f) \ (f " {0. }) ; :: thesis: x in dom F
A10: dom f c= C by RELAT_1:def 18;
A11: (dom f) \ (f " {0. }) c= C by A10, XBOOLE_1:1;
reconsider x = x as Element of C by A9, A11;
A12: x in (dom f) \ (f " {0. }) by A9;
thus x in dom F by A1, A12; :: thesis: verum

end;

A13: (dom f) \ (f " {0. }) c= dom F by A8, TARSKI:def 3;
thus dom F = (dom f) \ (f " {0. }) by A7, A13, XBOOLE_0:def 10; :: thesis: for c being Element of C st c in dom F holds
F . c = (R_EAL r) / (f . c)
let c be Element of C; :: thesis: ( c in dom F implies F . c = (R_EAL r) / (f . c) )
assume A14: c in dom F ; :: thesis: F . c = (R_EAL r) / (f . c)
thus F . c = (R_EAL r) / (f . c) by A2, A14; :: thesis: verum