set X = [.0,1.];
let f be bijective increasing UnOp of [.0,1.]; :: thesis: f " is increasing
A2: ((f | [.0,1.]) ") | (f .: [.0,1.]) is increasing by FC9;
A3: ( dom f = [.0,1.] & rng f = [.0,1.] ) by FUNCT_2:def 1, FUNCT_2:def 3;
f .: [.0,1.] = [.0,1.] by RELAT_1:113, A3;
hence f " is increasing by A2; :: thesis: verum