let p, g be Element of REAL ; :: thesis: for h being one-to-one PartFunc of REAL ,REAL st h | [.p,g.] is decreasing holds
((h | [.p,g.]) " ) | (h .: [.p,g.]) is decreasing
let h be one-to-one PartFunc of REAL ,REAL ; :: thesis: ( h | [.p,g.] is decreasing implies ((h | [.p,g.]) " ) | (h .: [.p,g.]) is decreasing )
assume that
A1: h | [.p,g.] is decreasing and
A2: not ((h | [.p,g.]) " ) | (h .: [.p,g.]) is decreasing ; :: thesis: contradiction
consider y1, y2 being Real such that
A3: ( y1 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) " )) & y2 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) " )) & y1 < y2 & ((h | [.p,g.]) " ) . y2 >= ((h | [.p,g.]) " ) . y1 ) by A2, Def3;
( y1 in h .: [.p,g.] & y2 in h .: [.p,g.] ) by A3, XBOOLE_0:def 4;
then A4: ( y1 in rng (h | [.p,g.]) & y2 in rng (h | [.p,g.]) ) by RELAT_1:148;
A5: (h | [.p,g.]) | [.p,g.] is decreasing by A1;

now

per cases ( ((h | [.p,g.]) " ) . y1 = ((h | [.p,g.]) " ) . y2 or ((h | [.p,g.]) " ) . y1 <> ((h | [.p,g.]) " ) . y2 ) ;

suppose ((h | [.p,g.]) " ) . y1 = ((h | [.p,g.]) " ) . y2 ; :: thesis: contradiction

then y1 = (h | [.p,g.]) . (((h | [.p,g.]) " ) . y2) by A4, FUNCT_1:57
.= y2 by A4, FUNCT_1:57 ;
hence contradiction by A3; :: thesis: verum

end;

suppose ((h | [.p,g.]) " ) . y1 <> ((h | [.p,g.]) " ) . y2 ; :: thesis: contradiction

then A6: ((h | [.p,g.]) " ) . y2 > ((h | [.p,g.]) " ) . y1 by A3, XXREAL_0:1;
A7: ( ((h | [.p,g.]) " ) . y2 in dom (h | [.p,g.]) & ((h | [.p,g.]) " ) . y1 in dom (h | [.p,g.]) ) by A4, PARTFUN2:79;
dom (h | [.p,g.]) = dom ((h | [.p,g.]) | [.p,g.]) by RELAT_1:101
.= [.p,g.] /\ (dom (h | [.p,g.])) by RELAT_1:90 ;
then (h | [.p,g.]) . (((h | [.p,g.]) " ) . y2) < (h | [.p,g.]) . (((h | [.p,g.]) " ) . y1) by A5, A6, A7, Def3;
then y2 < (h | [.p,g.]) . (((h | [.p,g.]) " ) . y1) by A4, FUNCT_1:57;
hence contradiction by A3, A4, FUNCT_1:57; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum