let f be bijective increasing UnOp of [.0,1.]; ((f | [.0,1.]) ") | (f .: [.0,1.]) is increasing
set X = [.0,1.];
assume A2:
not ((f | [.0,1.]) ") | (f .: [.0,1.]) is increasing
; contradiction
BB:
(f | [.0,1.]) " is REAL -defined
by Cosik1;
consider r1, r2 being Real such that
A3:
r1 in (f .: [.0,1.]) /\ (dom ((f | [.0,1.]) "))
and
A4:
r2 in (f .: [.0,1.]) /\ (dom ((f | [.0,1.]) "))
and
A5:
r1 < r2
and
A6:
((f | [.0,1.]) ") . r1 >= ((f | [.0,1.]) ") . r2
by A2, RF220, BB;
BB:
rng (f | [.0,1.]) c= [.0,1.]
by RELAT_1:def 19;
a1:
rng f c= [.0,1.]
by RELAT_1:def 19;
b2:
dom f = rng (f ")
by FUNCT_1:33;
b1:
rng f = dom (f ")
by FUNCT_1:33;
then a5:
dom ((f | [.0,1.]) ") = [.0,1.]
by FUNCT_2:def 1;
A7:
f .: [.0,1.] = rng (f | [.0,1.])
by RELAT_1:115;
then A8:
r1 in rng (f | [.0,1.])
by A3, XBOOLE_0:def 4;
A9:
r2 in rng (f | [.0,1.])
by A4, A7, XBOOLE_0:def 4;
A10:
(f | [.0,1.]) | [.0,1.] is increasing
;
now contradictionper cases
( ((f | [.0,1.]) ") . r1 = ((f | [.0,1.]) ") . r2 or ((f | [.0,1.]) ") . r1 <> ((f | [.0,1.]) ") . r2 )
;
suppose A11:
((f | [.0,1.]) ") . r1 <> ((f | [.0,1.]) ") . r2
;
contradictionreconsider d =
r2 as
Element of
[.0,1.] by BB, A9;
set c =
((f | [.0,1.]) ") . d;
a4:
rng ((f | [.0,1.]) ") c= [.0,1.]
by b2, RELAT_1:def 19;
((f | [.0,1.]) ") . d in rng ((f | [.0,1.]) ")
by a5, FUNCT_1:3;
then reconsider c =
((f | [.0,1.]) ") . d as
Element of
[.0,1.] by a4;
F1:
(
r2 in rng f &
c = (f ") . r2 implies
c in dom f )
by PARTFUN2:60;
reconsider rr1 =
r1 as
Element of
[.0,1.] by A8, a1;
aa:
(
rr1 in rng f implies
(f ") . rr1 in dom f )
by PARTFUN2:60;
((f | [.0,1.]) ") . r2 < ((f | [.0,1.]) ") . r1
by A6, A11, XXREAL_0:1;
then
(f | [.0,1.]) . (((f | [.0,1.]) ") . r2) < (f | [.0,1.]) . (((f | [.0,1.]) ") . r1)
by A10, aa, A4, A7, XBOOLE_0:def 4, F1, A3;
then
r2 < (f | [.0,1.]) . (((f | [.0,1.]) ") . r1)
by A9, FUNCT_1:35;
hence
contradiction
by A5, A8, FUNCT_1:35;
verum end;
hence
contradiction
; verum