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 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