set N = N_CC ;
set f = (AffineMap ((- 1),1)) | [.0,1.];
A2: dom (AffineMap ((- 1),1)) = REAL by FUNCT_2:def 1;
AA: dom N_CC = dom ((AffineMap ((- 1),1)) | [.0,1.]) by A2, FUNCT_2:def 1;
for x being object st x in dom N_CC holds
((AffineMap ((- 1),1)) | [.0,1.]) . x = N_CC . x

proof

let x be object ; :: thesis: ( x in dom N_CC implies ((AffineMap ((- 1),1)) | [.0,1.]) . x = N_CC . x )
assume x in dom N_CC ; :: thesis: ((AffineMap ((- 1),1)) | [.0,1.]) . x = N_CC . x
then reconsider xx = x as Element of [.0,1.] by FUNCT_2:def 1;
((AffineMap ((- 1),1)) | [.0,1.]) . x = (AffineMap ((- 1),1)) . xx by FUNCT_1:49
.= ((- 1) * xx) + 1 by FCONT_1:def 4
.= 1 - xx
.= N_CC . x by FUZIMPL3:def 6 ;
hence ((AffineMap ((- 1),1)) | [.0,1.]) . x = N_CC . x ; :: thesis: verum

end;

hence N_CC = (AffineMap ((- 1),1)) | [.0,1.] by AA, FUNCT_1:2; :: thesis: verum