deffunc H₁( set ) -> Real = max+ (F . $1);
defpred S₁[ set ] means $1 in dom F;
consider f being PartFunc of D,REAL such that
A1: for d being Element of D holds
( d in dom f iff S₁[d] ) and
A2: for d being Element of D st d in dom f holds
f . d = H₁(d) from SEQ_1:sch 3();
take f ; :: thesis: ( dom f = dom F & ( for d being Element of D st d in dom f holds
f . d = max+ (F . d) ) )
thus dom f = dom F :: thesis: for d being Element of D st d in dom f holds
f . d = max+ (F . d)

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 x in dom f ; :: thesis: x in dom F
hence x in dom F by A1; :: thesis: verum

end;

let x be set ; :: 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;

thus for d being Element of D st d in dom f holds
f . d = max+ (F . d) by A2; :: thesis: verum