defpred S1[ 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 S1[c] ) and
A2: for c being Element of C st c in dom F holds
F . c = H1(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 by A1; :: according to XBOOLE_0:def 10 :: thesis: dom f c= dom F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in dom F )
assume x in dom f ; :: thesis: x in dom F
hence x in dom F by A1; :: thesis: verum
end;
let c be Element of C; :: thesis: ( c in dom F implies F . c = max ((f . c),0.) )
assume c in dom F ; :: thesis: F . c = max ((f . c),0.)
hence F . c = max ((f . c),0.) by A2; :: thesis: verum