let g, p be 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, Th21;
y1 in h .: [.p,g.] by A3, XBOOLE_0:def 4;
then A7: y1 in rng (h | [.p,g.]) by RELAT_1:115;
y2 in h .: [.p,g.] by A4, XBOOLE_0:def 4;
then A8: y2 in rng (h | [.p,g.]) by RELAT_1:115;
A9: (h | [.p,g.]) | [.p,g.] is decreasing by A1;

now :: thesis: contradiction

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:35
.= y2 by A8, FUNCT_1:35 ;
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:72
.= [.p,g.] /\ (dom (h | [.p,g.])) by RELAT_1:61 ;
( ((h | [.p,g.]) ") . y2 in REAL & ((h | [.p,g.]) ") . y1 in REAL & y1 in REAL & y2 in REAL ) by XREAL_0:def 1;
then A12: ( ((h | [.p,g.]) ") . y2 in dom (h | [.p,g.]) & ((h | [.p,g.]) ") . y1 in dom (h | [.p,g.]) ) by A7, A8, PARTFUN2:60;
((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, Th21;
then y2 < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A8, FUNCT_1:35;
hence contradiction by A5, A7, FUNCT_1:35; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum