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;
now :: thesis: contradiction
per cases ( ((f | X) ") . r1 = ((f | X) ") . r2 or ((f | X) ") . r1 <> ((f | X) ") . r2 ) ;
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;
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;
end;
end;
hence contradiction ; :: thesis: verum