set f = N_CC ;
set g = SugenoNegation 0;
for x being object st x in [.0,1.] holds
N_CC . x = (SugenoNegation 0) . x

proof

let x be object ; :: thesis: ( x in [.0,1.] implies N_CC . x = (SugenoNegation 0) . x )
assume x in [.0,1.] ; :: thesis: N_CC . x = (SugenoNegation 0) . x
then reconsider xx = x as Element of [.0,1.] ;
(SugenoNegation 0) . xx = (1 - xx) / (1 + (0 * xx)) by DefSugeno
.= N_CC . xx by NDef ;
hence N_CC . x = (SugenoNegation 0) . x ; :: thesis: verum

end;

hence N_CC = SugenoNegation 0 by FUNCT_2:12; :: thesis: verum