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

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 end;

hence
f | X is one-to-one
; :: thesis: verumper cases
( f | X is increasing or f | X is decreasing )
by A1;

end;

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

end;

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 )

hence
f | X is one-to-one
by PARTFUN1:8; :: thesis: verum( 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;

end;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: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( r1 < r2 or r2 < r1 )
by A6, XXREAL_0:1;

end;

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;then (f | X) . r1 < f . r2 by A3, FUNCT_1:47;

hence contradiction by A4, A5, FUNCT_1:47; :: thesis: verum

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;then (f | X) . r2 < f . r1 by A4, FUNCT_1:47;

hence contradiction by A3, A5, FUNCT_1:47; :: thesis: verum

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

end;

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 )

hence
f | X is one-to-one
by PARTFUN1:8; :: thesis: verum( 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;

end;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: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( r1 < r2 or r2 < r1 )
by A12, XXREAL_0:1;

end;

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;then (f | X) . r2 < f . r1 by A10, FUNCT_1:47;

hence contradiction by A9, A11, FUNCT_1:47; :: thesis: verum

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;then (f | X) . r1 < f . r2 by A9, FUNCT_1:47;

hence contradiction by A10, A11, FUNCT_1:47; :: thesis: verum