set N = N_CC ;
set I = I_RC ;
for x, y being Element of [.0,1.] holds I_RC . (x,y) = I_RC . ((N_CC . y),(N_CC . x))

proof

let x, y be Element of [.0,1.]; :: thesis: I_RC . (x,y) = I_RC . ((N_CC . y),(N_CC . x))
SA: N_CC . x = 1 - x by FUZIMPL3:def 6;
SB: N_CC . y = 1 - y by FUZIMPL3:def 6;
I_RC . (x,y) = (1 - x) + (x * y) by FUZIMPL1:def 17
.= (1 - (N_CC . y)) + ((N_CC . y) * (N_CC . x)) by SA, SB
.= I_RC . ((N_CC . y),(N_CC . x)) by FUZIMPL1:def 17 ;
hence I_RC . (x,y) = I_RC . ((N_CC . y),(N_CC . x)) ; :: thesis: verum

end;

hence I_RC is N_CC -satisfying_CP ; :: thesis: verum