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.]) " )) and
A4: y2 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) " )) and
A5: y1 < y2 and
A6: ((h | [.p,g.]) " ) . y2 >= ((h | [.p,g.]) " ) . y1 by A2, Th44;
y1 in h .: [.p,g.] by A3, XBOOLE_0:def 4;
then A7: y1 in rng (h | [.p,g.]) by RELAT_1:148;
y2 in h .: [.p,g.] by A4, XBOOLE_0:def 4;
then A8: y2 in rng (h | [.p,g.]) by RELAT_1:148;
A9: (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 A7, FUNCT_1:57
.= y2 by A8, FUNCT_1:57 ;
hence contradiction by A5; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum