defpred S₁[ Element of C] means $1 in dom f;
consider F being PartFunc of C,ExtREAL such that
A6: for c being Element of C holds
( c in dom F iff S₁[c] ) and
A7: 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 x being Element of C st x in dom F holds
F . x = max (- (f . x)),0. ) )
thus dom F = dom f :: thesis: for x being Element of C st x in dom F holds
F . x = max (- (f . x)),0.

proof

thus dom F c= dom f :: according to XBOOLE_0:def 10 :: thesis: dom f c= dom F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom F or x in dom f )
assume A8: x in dom F ; :: thesis: x in dom f
thus x in dom f by A6, A8; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom F )
assume A9: x in dom f ; :: thesis: x in dom F
thus x in dom F by A6, A9; :: thesis: verum

end;

let c be Element of C; :: thesis: ( c in dom F implies F . c = max (- (f . c)),0. )
assume A10: c in dom F ; :: thesis: F . c = max (- (f . c)),0.
thus F . c = max (- (f . c)),0. by A7, A10; :: thesis: verum