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 }
set li = right_closed_halfline 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 set ; :: 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 ;
A4: ( d in dom F & F . d in right_closed_halfline 0 ) by A3, FUNCT_1:def 13;
then ex s being Real st
( s = F . d & 0 <= s ) by A2;
then - (F . d) <= - 0 ;
then A5: max (- (F . d)),0 = 0 by XXREAL_0:def 10;
(max- F) . d = max- (F . d) by A1, A4, Def11
.= max (- (F . d)),0 ;
then (max- F) . d in {0 } by A5, TARSKI:def 1;
hence x in (max- F) " {0 } by A1, A4, 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 " (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 ;
A7: ( d in dom F & (max- F) . d in {0 } ) by A1, A6, FUNCT_1:def 13;
then A8: (max- F) . d = 0 by TARSKI:def 1;
(max- F) . d = max- (F . d) by A1, A7, Def11
.= max (- (F . d)),0 ;
then - (F . d) <= - 0 by A8, XXREAL_0:def 10;
then 0 <= F . d by XREAL_1:26;
then F . d in right_closed_halfline 0 by A2;
hence x in F " (right_closed_halfline 0 ) by A7, FUNCT_1:def 13; :: thesis: verum