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 ;
A7: f .: X = rng (f | X) by RELAT_1:115;
then A8: r1 in rng (f | X) by ;
A9: r2 in rng (f | X) by ;
A10: (f | X) | X is decreasing by A1;
now :: thesis: contradiction
per cases ) ") . 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
.= r2 by ;
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 ;
((f | X) ") . r2 > ((f | X) ") . r1 by ;
then (f | X) . (((f | X) ") . r2) < (f | X) . (((f | X) ") . r1) by ;
then r2 < (f | X) . (((f | X) ") . r1) by ;
hence contradiction by A5, A8, FUNCT_1:35; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum