defpred S_{1}[ Element of C] means $1 in dom f;

consider F being PartFunc of C,ExtREAL such that

A3: for c being Element of C holds

( c in dom F iff S_{1}[c] )
and

A4: for c being Element of C st c in dom F holds

F . c = H_{2}(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.)

assume c in dom F ; :: thesis: F . c = max ((- (f . c)),0.)

hence F . c = max ((- (f . c)),0.) by A4; :: thesis: verum

consider F being PartFunc of C,ExtREAL such that

A3: for c being Element of C holds

( c in dom F iff S

A4: for c being Element of C st c in dom F holds

F . c = H

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

let c be Element of C; :: thesis: ( c in dom F implies F . c = max ((- (f . c)),0.) )
thus
dom F c= dom f
by A3; :: 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 A3; :: thesis: verum

end;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 A3; :: thesis: verum

assume c in dom F ; :: thesis: F . c = max ((- (f . c)),0.)

hence F . c = max ((- (f . c)),0.) by A4; :: thesis: verum