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

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I_FD) . x = N_CC . x
1 - x in [.0,1.] by FUZNORM1:7;
then A2: 1 - x >= 0 by XXREAL_1:1;

per cases ( x <= 0 or x > 0 ) ;

suppose x <= 0 ; :: thesis: (FNegation I_FD) . x = N_CC . x

then B2: x = 0 by XXREAL_1:1;
(FNegation I_FD) . x = I_FD . (x,0) by FNeg
.= 1 - x by FUZIMPL1:def 23, B2
.= N_CC . x by NDef ;
hence (FNegation I_FD) . x = N_CC . x ; :: thesis: verum

end;

suppose B1: x > 0 ; :: thesis: (FNegation I_FD) . x = N_CC . x

(FNegation I_FD) . x = I_FD . (x,0) by FNeg
.= max ((1 - x),0) by A1, B1, FUZIMPL1:def 23
.= 1 - x by XXREAL_0:def 10, A2
.= N_CC . x by NDef ;
hence (FNegation I_FD) . x = N_CC . x ; :: thesis: verum

end;

end;

end;

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