let g, p be Real; :: thesis: for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is increasing holds
((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing
let h be one-to-one PartFunc of REAL,REAL; :: thesis: ( h | [.p,g.] is increasing implies ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing )
assume that
A1: h | [.p,g.] is increasing and
A2: not ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing ; :: 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.]) ") . y1 >= ((h | [.p,g.]) ") . y2 by A2, Th20;
reconsider yy1 = y1, yy2 = y2 as Real ;
y1 in h .: [.p,g.] by A3, XBOOLE_0:def 4;
then A7: yy1 in rng (h | [.p,g.]) by RELAT_1:115;
y2 in h .: [.p,g.] by A4, XBOOLE_0:def 4;
then A8: yy2 in rng (h | [.p,g.]) by RELAT_1:115;
A9: (h | [.p,g.]) | [.p,g.] is increasing by A1;

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.]) ") . yy2 in REAL & ((h | [.p,g.]) ") . yy1 in REAL ) by XREAL_0:def 1;
then A12: ( ((h | [.p,g.]) ") . yy2 in dom (h | [.p,g.]) & ((h | [.p,g.]) ") . yy1 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, Th20;
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;