let h be PartFunc of REAL,REAL; :: thesis: ( h is non-decreasing & h is non-increasing implies h is V8() )
assume A1: ( h is non-decreasing & h is non-increasing ) ; :: thesis: h is V8()
let r1, r2 be object ; :: according to FUNCT_1:def 10 :: thesis: ( not r1 in dom h or not r2 in dom h or h . r1 = h . r2 )
assume A2: ( r1 in dom h & r2 in dom h ) ; :: thesis: h . r1 = h . r2
then reconsider r1 = r1, r2 = r2 as Real ;
( r1 < r2 or r1 = r2 or r2 < r1 ) by XXREAL_0:1;
then ( h . r1 <= h . r2 & h . r2 <= h . r1 ) by A1, A2;
hence h . r1 = h . r2 by XXREAL_0:1; :: thesis: verum