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

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

given r1, r2 being Real such that A3: ( r1 in dom (f | X) & r2 in dom (f | X) & (f | X) . r1 = (f | X) . r2 ) and
A4: r1 <> r2 ; :: thesis: contradiction
A5: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A3, RELAT_1:90;

now

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

suppose r1 < r2 ; :: thesis: contradiction

then f . r1 < f . r2 by A2, A5, RFUNCT_2:43;
then (f | X) . r1 < f . r2 by A3, FUNCT_1:70;
hence contradiction by A3, FUNCT_1:70; :: thesis: verum

end;

suppose r2 < r1 ; :: thesis: contradiction

then f . r2 < f . r1 by A2, A5, RFUNCT_2:43;
then (f | X) . r2 < f . r1 by A3, FUNCT_1:70;
hence contradiction by A3, FUNCT_1:70; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

end;

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

now

given r1, r2 being Real such that A7: ( r1 in dom (f | X) & r2 in dom (f | X) & (f | X) . r1 = (f | X) . r2 ) and
A8: r1 <> r2 ; :: thesis: contradiction
A9: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A7, RELAT_1:90;

now

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

suppose r1 < r2 ; :: thesis: contradiction

then f . r2 < f . r1 by A6, A9, RFUNCT_2:44;
then (f | X) . r2 < f . r1 by A7, FUNCT_1:70;
hence contradiction by A7, FUNCT_1:70; :: thesis: verum

end;

suppose r2 < r1 ; :: thesis: contradiction

then f . r1 < f . r2 by A6, A9, RFUNCT_2:44;
then (f | X) . r1 < f . r2 by A7, FUNCT_1:70;
hence contradiction by A7, FUNCT_1:70; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

end;

end;

end;

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