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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F " (right_closed_halfline 0) or x in (max- F) " {0} )
assume A3: x in F " (right_closed_halfline 0) ; :: thesis: x in (max- F) " {0}
then reconsider d = x as Element of D ;
F . d in right_closed_halfline 0 by A3, FUNCT_1:def 7;
then ex s being Real st
( s = F . d & 0 <= s ) 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, Def11
.= 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 " (right_closed_halfline 0) )
assume A6: x in (max- F) " {0} ; :: thesis: x in F " (right_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, Def11
.= max ((- (F . d)),0) ;
then - (F . d) <= - 0 by A7, XXREAL_0:def 10;
then 0 <= F . d by XREAL_1:24;
then F . d in right_closed_halfline 0 by A2;
hence x in F " (right_closed_halfline 0) by A8, FUNCT_1:def 7; :: thesis: verum