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

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I_LK) . x = N_CC . x
1 - x in [.0,1.] by FUZNORM1:7;
then A2: 1 - x <= 1 by XXREAL_1:1;
(FNegation I_LK) . x = I_LK . (x,0) by FNeg
.= min (1,((1 - x) + 0)) by A1, FUZIMPL1:def 14
.= 1 - x by A2, XXREAL_0:def 9
.= N_CC . x by NDef ;
hence (FNegation I_LK) . x = N_CC . x ; :: thesis: verum

end;

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