set f = N_CC ;
B1: [.0,1.] c= rng N_CC
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.0,1.] or x in rng N_CC )
assume x in [.0,1.] ; :: thesis: x in rng N_CC
then reconsider xx = x as Element of [.0,1.] ;
set y = 1 - xx;
B3: 1 - xx in [.0,1.] by FUZNORM1:7;
then B2: 1 - xx in dom N_CC by FUNCT_2:def 1;
N_CC . (1 - xx) = 1 - (1 - xx) by NDef, B3
.= xx ;
hence x in rng N_CC by B2, FUNCT_1:def 3; :: thesis: verum
end;
a0: rng N_CC c= [.0,1.] by RELAT_1:def 19;
for x1, x2 being object st x1 in dom N_CC & x2 in dom N_CC & N_CC . x1 = N_CC . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom N_CC & x2 in dom N_CC & N_CC . x1 = N_CC . x2 implies x1 = x2 )
assume A1: ( x1 in dom N_CC & x2 in dom N_CC & N_CC . x1 = N_CC . x2 ) ; :: thesis: x1 = x2
then reconsider xx1 = x1, xx2 = x2 as Element of [.0,1.] by FUNCT_2:def 1;
( N_CC . xx1 = 1 - xx1 & N_CC . xx2 = 1 - xx2 ) by NDef;
then 1 - xx1 = 1 - xx2 by A1;
hence x1 = x2 ; :: thesis: verum
end;
then ( N_CC is one-to-one & N_CC is onto ) by a0, FUNCT_1:def 4, FUNCT_2:def 3, B1, XBOOLE_0:def 10;
hence N_CC is bijective ; :: thesis: N_CC is decreasing
for a, b being Element of [.0,1.] st a < b holds
N_CC . a > N_CC . b
proof
let a, b be Element of [.0,1.]; :: thesis: ( a < b implies N_CC . a > N_CC . b )
assume S0: a < b ; :: thesis: N_CC . a > N_CC . b
S1: ( N_CC . a = 1 - a & N_CC . b = 1 - b ) by NDef;
- a > - b by S0, XREAL_1:24;
hence N_CC . a > N_CC . b by S1, XREAL_1:6; :: thesis: verum
end;
hence N_CC is decreasing by Decreas; :: thesis: verum