let X be set ; :: thesis: for f being PartFunc of REAL,REAL st ( f | X is increasing or f | X is decreasing ) holds
f | X is one-to-one
let f be PartFunc of REAL,REAL; :: thesis: ( ( f | X is increasing or f | X is decreasing ) implies f | X is one-to-one )
assume A1: ( f | X is increasing or f | X is decreasing ) ; :: thesis: f | X is one-to-one

now :: thesis: f | X is one-to-one

per cases ( f | X is increasing or f | X is decreasing ) by A1;

suppose A2: f | X is increasing ; :: thesis: f | X is one-to-one

now :: thesis: for r1, r2 being Element of REAL holds
( not r1 in dom (f | X) or not r2 in dom (f | X) or not (f | X) . r1 = (f | X) . r2 or not r1 <> r2 )

given r1, r2 being Element of REAL such that A3: r1 in dom (f | X) and
A4: r2 in dom (f | X) and
A5: (f | X) . r1 = (f | X) . r2 and
A6: r1 <> r2 ; :: thesis: contradiction
A7: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A3, A4, RELAT_1:61;

now :: thesis: contradiction

per cases ( r1 < r2 or r2 < r1 ) by A6, XXREAL_0:1;

suppose r1 < r2 ; :: thesis: contradiction

then f . r1 < f . r2 by A2, A7, RFUNCT_2:20;
then (f | X) . r1 < f . r2 by A3, FUNCT_1:47;
hence contradiction by A4, A5, FUNCT_1:47; :: thesis: verum

end;

suppose r2 < r1 ; :: thesis: contradiction

then f . r2 < f . r1 by A2, A7, RFUNCT_2:20;
then (f | X) . r2 < f . r1 by A4, FUNCT_1:47;
hence contradiction by A3, A5, FUNCT_1:47; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence f | X is one-to-one by PARTFUN1:8; :: thesis: verum

end;

suppose A8: f | X is decreasing ; :: thesis: f | X is one-to-one

now :: thesis: for r1, r2 being Element of REAL holds
( not r1 in dom (f | X) or not r2 in dom (f | X) or not (f | X) . r1 = (f | X) . r2 or not r1 <> r2 )

given r1, r2 being Element of REAL such that A9: r1 in dom (f | X) and
A10: r2 in dom (f | X) and
A11: (f | X) . r1 = (f | X) . r2 and
A12: r1 <> r2 ; :: thesis: contradiction
A13: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A9, A10, RELAT_1:61;

now :: thesis: contradiction

per cases ( r1 < r2 or r2 < r1 ) by A12, XXREAL_0:1;

suppose r1 < r2 ; :: thesis: contradiction

then f . r2 < f . r1 by A8, A13, RFUNCT_2:21;
then (f | X) . r2 < f . r1 by A10, FUNCT_1:47;
hence contradiction by A9, A11, FUNCT_1:47; :: thesis: verum

end;

suppose r2 < r1 ; :: thesis: contradiction

then f . r1 < f . r2 by A8, A13, RFUNCT_2:21;
then (f | X) . r1 < f . r2 by A9, FUNCT_1:47;
hence contradiction by A10, A11, FUNCT_1:47; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence f | X is one-to-one by PARTFUN1:8; :: thesis: verum

end;

end;

end;

hence f | X is one-to-one ; :: thesis: verum