set li = left_closed_halfline 0;
let D be non empty set ; :: thesis: for F being PartFunc of D,REAL holds F " (left_closed_halfline 0) = (max+ F) " {0}
let F be PartFunc of D,REAL; :: thesis: F " (left_closed_halfline 0) = (max+ F) " {0}
A1: dom (max+ F) = dom F by Def10;
A2: left_closed_halfline 0 = { s where s is Real : s <= 0 } by XXREAL_1:231;
thus F " (left_closed_halfline 0) c= (max+ F) " {0} :: according to XBOOLE_0:def 10 :: thesis: (max+ F) " {0} c= F " (left_closed_halfline 0)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F " (left_closed_halfline 0) or x in (max+ F) " {0} )
assume A3: x in F " (left_closed_halfline 0) ; :: thesis: x in (max+ F) " {0}
then reconsider d = x as Element of D ;
F . d in left_closed_halfline 0 by A3, FUNCT_1:def 7;
then ex s being Real st
( s = F . d & s <= 0 ) by A2;
then A4: max ((F . d),0) = 0 by XXREAL_0:def 10;
A5: d in dom F by A3, FUNCT_1:def 7;
then (max+ F) . d = max+ (F . d) by A1, Def10
.= max ((F . d),0) ;
then (max+ F) . d in {0} by A4, TARSKI:def 1;
hence x in (max+ F) " {0} by A1, A5, FUNCT_1:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (max+ F) " {0} or x in F " (left_closed_halfline 0) )
assume A6: x in (max+ F) " {0} ; :: thesis: x in F " (left_closed_halfline 0)
then reconsider d = x as Element of D ;
(max+ F) . d in {0} by A6, FUNCT_1:def 7;
then A7: (max+ F) . d = 0 by TARSKI:def 1;
A8: d in dom F by A1, A6, FUNCT_1:def 7;
then (max+ F) . d = max+ (F . d) by A1, Def10
.= max ((F . d),0) ;
then F . d <= 0 by A7, XXREAL_0:def 10;
then F . d in left_closed_halfline 0 by A2;
hence x in F " (left_closed_halfline 0) by A8, FUNCT_1:def 7; :: thesis: verum