let X be set ; :: thesis: for f being one-to-one PartFunc of REAL,REAL st f | X is decreasing holds

((f | X) ") | (f .: X) is decreasing

let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( f | X is decreasing implies ((f | X) ") | (f .: X) is decreasing )

assume that

A1: f | X is decreasing and

A2: not ((f | X) ") | (f .: X) is decreasing ; :: thesis: contradiction

consider r1, r2 being Real such that

A3: r1 in (f .: X) /\ (dom ((f | X) ")) and

A4: r2 in (f .: X) /\ (dom ((f | X) ")) and

A5: r1 < r2 and

A6: ((f | X) ") . r1 <= ((f | X) ") . r2 by A2, RFUNCT_2:21;

A7: f .: X = rng (f | X) by RELAT_1:115;

then A8: r1 in rng (f | X) by A3, XBOOLE_0:def 4;

A9: r2 in rng (f | X) by A4, A7, XBOOLE_0:def 4;

A10: (f | X) | X is decreasing by A1;

((f | X) ") | (f .: X) is decreasing

let f be one-to-one PartFunc of REAL,REAL; :: thesis: ( f | X is decreasing implies ((f | X) ") | (f .: X) is decreasing )

assume that

A1: f | X is decreasing and

A2: not ((f | X) ") | (f .: X) is decreasing ; :: thesis: contradiction

consider r1, r2 being Real such that

A3: r1 in (f .: X) /\ (dom ((f | X) ")) and

A4: r2 in (f .: X) /\ (dom ((f | X) ")) and

A5: r1 < r2 and

A6: ((f | X) ") . r1 <= ((f | X) ") . r2 by A2, RFUNCT_2:21;

A7: f .: X = rng (f | X) by RELAT_1:115;

then A8: r1 in rng (f | X) by A3, XBOOLE_0:def 4;

A9: r2 in rng (f | X) by A4, A7, XBOOLE_0:def 4;

A10: (f | X) | X is decreasing by A1;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ((f | X) ") . r1 = ((f | X) ") . r2 or ((f | X) ") . r1 <> ((f | X) ") . r2 )
;

end;

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

then r1 =
(f | X) . (((f | X) ") . r2)
by A8, FUNCT_1:35

.= r2 by A9, FUNCT_1:35 ;

hence contradiction by A5; :: thesis: verum

end;.= r2 by A9, FUNCT_1:35 ;

hence contradiction by A5; :: thesis: verum

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

A12: dom (f | X) =
dom ((f | X) | X)

.= X /\ (dom (f | X)) by RELAT_1:61 ;

( r1 in REAL & r2 in REAL & ((f | X) ") . r2 in REAL & ((f | X) ") . r1 in REAL ) by XREAL_0:def 1;

then A13: ( ((f | X) ") . r2 in dom (f | X) & ((f | X) ") . r1 in dom (f | X) ) by A8, A9, PARTFUN2:60;

((f | X) ") . r2 > ((f | X) ") . r1 by A6, A11, XXREAL_0:1;

then (f | X) . (((f | X) ") . r2) < (f | X) . (((f | X) ") . r1) by A10, A13, A12, RFUNCT_2:21;

then r2 < (f | X) . (((f | X) ") . r1) by A9, FUNCT_1:35;

hence contradiction by A5, A8, FUNCT_1:35; :: thesis: verum

end;.= X /\ (dom (f | X)) by RELAT_1:61 ;

( r1 in REAL & r2 in REAL & ((f | X) ") . r2 in REAL & ((f | X) ") . r1 in REAL ) by XREAL_0:def 1;

then A13: ( ((f | X) ") . r2 in dom (f | X) & ((f | X) ") . r1 in dom (f | X) ) by A8, A9, PARTFUN2:60;

((f | X) ") . r2 > ((f | X) ") . r1 by A6, A11, XXREAL_0:1;

then (f | X) . (((f | X) ") . r2) < (f | X) . (((f | X) ") . r1) by A10, A13, A12, RFUNCT_2:21;

then r2 < (f | X) . (((f | X) ") . r1) by A9, FUNCT_1:35;

hence contradiction by A5, A8, FUNCT_1:35; :: thesis: verum