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

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I_RC) . x = N_CC . x
(FNegation I_RC) . x = I_RC . (x,0) by FNeg
.= (1 - x) + (x * 0) by FUZIMPL1:def 17, A1
.= N_CC . x by NDef ;
hence (FNegation I_RC) . x = N_CC . x ; :: thesis: verum

end;

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