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 set ; :: 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 13;
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 13;
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 13; :: thesis: verum

end;

let x be set ; :: 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 13;
then A7: (max+ F) . d = 0 by TARSKI:def 1;
A8: d in dom F by A1, A6, FUNCT_1:def 13;
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 13; :: thesis: verum