let X be set ; for f being one-to-one PartFunc of REAL,REAL st f | X is increasing holds
((f | X) ") | (f .: X) is increasing
let f be one-to-one PartFunc of REAL,REAL; ( f | X is increasing implies ((f | X) ") | (f .: X) is increasing )
assume that
A1:
f | X is increasing
and
A2:
not ((f | X) ") | (f .: X) is increasing
; 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:20;
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 increasing
by A1;
now contradictionper cases
( ((f | X) ") . r1 = ((f | X) ") . r2 or ((f | X) ") . r1 <> ((f | X) ") . r2 )
;
suppose A11:
((f | X) ") . r1 <> ((f | X) ") . r2
;
contradictionA12:
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:20;
then
r2 < (f | X) . (((f | X) ") . r1)
by A9, FUNCT_1:35;
hence
contradiction
by A5, A8, FUNCT_1:35;
verum end; end; end;
hence
contradiction
; verum