let f be bijective increasing UnOp of [.0,1.]; :: thesis: ((f | [.0,1.]) ") | (f .: [.0,1.]) is increasing
set X = [.0,1.];
assume A2: not ((f | [.0,1.]) ") | (f .: [.0,1.]) is increasing ; :: thesis: 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;
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 :: thesis: contradiction

per cases ( ((f | [.0,1.]) ") . r1 = ((f | [.0,1.]) ") . r2 or ((f | [.0,1.]) ") . r1 <> ((f | [.0,1.]) ") . r2 ) ;

suppose ((f | [.0,1.]) ") . r1 = ((f | [.0,1.]) ") . r2 ; :: thesis: contradiction

then r1 = (f | [.0,1.]) . (((f | [.0,1.]) ") . r2) by A8, FUNCT_1:35
.= r2 by A9, FUNCT_1:35 ;
hence contradiction by A5; :: thesis: verum

end;

suppose A11: ((f | [.0,1.]) ") . r1 <> ((f | [.0,1.]) ") . r2 ; :: thesis: contradiction

reconsider 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; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum