let X be set ; :: thesis: for f being one-to-one PartFunc of REAL ,REAL st f | X is increasing holds
((f | X) " ) | (f .: X) is increasing
let f be one-to-one PartFunc of REAL ,REAL ; :: thesis: ( f | X is increasing implies ((f | X) " ) | (f .: X) is increasing )
assume that
A1: f | X is increasing and
A2: not ((f | X) " ) | (f .: X) is increasing ; :: thesis: contradiction
consider r1, r2 being Real such that
A3: ( r1 in (f .: X) /\ (dom ((f | X) " )) & r2 in (f .: X) /\ (dom ((f | X) " )) & r1 < r2 & ((f | X) " ) . r1 >= ((f | X) " ) . r2 ) by A2, RFUNCT_2:43;
f .: X = rng (f | X) by RELAT_1:148;
then A4: ( r1 in rng (f | X) & r2 in rng (f | X) ) by A3, XBOOLE_0:def 4;
A5: (f | X) | X is increasing by A1;

now

per cases ( ((f | X) " ) . r1 = ((f | X) " ) . r2 or ((f | X) " ) . r1 <> ((f | X) " ) . r2 ) ;

suppose ((f | X) " ) . r1 = ((f | X) " ) . r2 ; :: thesis: contradiction

then r1 = (f | X) . (((f | X) " ) . r2) by A4, FUNCT_1:57
.= r2 by A4, FUNCT_1:57 ;
hence contradiction by A3; :: thesis: verum

end;

suppose ((f | X) " ) . r1 <> ((f | X) " ) . r2 ; :: thesis: contradiction

then A6: ((f | X) " ) . r2 < ((f | X) " ) . r1 by A3, XXREAL_0:1;
A7: ( ((f | X) " ) . r2 in dom (f | X) & ((f | X) " ) . r1 in dom (f | X) ) by A4, PARTFUN2:79;
dom (f | X) = dom ((f | X) | X) by RELAT_1:101
.= X /\ (dom (f | X)) by RELAT_1:90 ;
then (f | X) . (((f | X) " ) . r2) < (f | X) . (((f | X) " ) . r1) by A5, A6, A7, RFUNCT_2:43;
then r2 < (f | X) . (((f | X) " ) . r1) by A4, FUNCT_1:57;
hence contradiction by A3, A4, FUNCT_1:57; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum