defpred S₁[ Element of C] means $1 in dom f;
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 & ( for c being Element of C st c in dom F holds
F . c = (R_EAL r) * (f . c) ) )
for x being set st x in dom F holds
x in dom f

proof

let x be set ; :: thesis: ( x in dom F implies x in dom f )
assume A4: x in dom F ; :: thesis: x in dom f
dom F c= C by RELAT_1:def 18;
then reconsider x = x as Element of C by A4;
x in dom F by A4;
hence x in dom f by A1; :: thesis: verum

end;

then A7: dom F c= dom f by TARSKI:def 3;
for x being set st x in dom f holds
x in dom F

proof

let x be set ; :: thesis: ( x in dom f implies x in dom F )
assume A9: x in dom f ; :: thesis: x in dom F
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 F by A1; :: thesis: verum

end;

then dom f c= dom F by TARSKI:def 3;
hence dom F = dom f by A7, 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 c in dom F ; :: thesis: F . c = (R_EAL r) * (f . c)
hence F . c = (R_EAL r) * (f . c) by A2; :: thesis: verum