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 ;
now :: thesis: contradiction
per cases ( r1 < r2 or r2 < r1 ) by ;
suppose r1 < r2 ; :: thesis: contradiction
then f . r1 < f . r2 by ;
then (f | X) . r1 < f . r2 by ;
hence contradiction by A4, A5, FUNCT_1:47; :: thesis: verum
end;
suppose r2 < r1 ; :: thesis: contradiction
then f . r2 < f . r1 by ;
then (f | X) . r2 < f . r1 by ;
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 ;
now :: thesis: contradiction
per cases ( r1 < r2 or r2 < r1 ) by ;
suppose r1 < r2 ; :: thesis: contradiction
then f . r2 < f . r1 by ;
then (f | X) . r2 < f . r1 by ;
hence contradiction by A9, A11, FUNCT_1:47; :: thesis: verum
end;
suppose r2 < r1 ; :: thesis: contradiction
then f . r1 < f . r2 by ;
then (f | X) . r1 < f . r2 by ;
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