set I = I_KD ;
set f = FNegation I_KD;
set g = N_CC ;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds (FNegation I_KD) . x = N_CC . x

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I_KD) . x = N_CC . x
1 - x in [.0,1.] by FUZNORM1:7;
then A2: 1 - x >= 0 by XXREAL_1:1;
(FNegation I_KD) . x = I_KD . (x,0) by FNeg
.= max ((1 - x),0) by FUZIMPL1:def 18, A1
.= 1 - x by A2, XXREAL_0:def 10
.= N_CC . x by NDef ;
hence (FNegation I_KD) . x = N_CC . x ; :: thesis: verum

end;

hence FNegation I_KD = N_CC by FUNCT_2:63; :: thesis: verum