reconsider g = L[01] (((0,1) (#)),((#) (0,1))) as Function of I[01],I[01] by TOPMETR:20;
set t1 = (0,1) (#) ;
set t2 = (#) (0,1);
set f = L[01] (((0,1) (#)),((#) (0,1)));
L[01] (((0,1) (#)),((#) (0,1))) = N_CC

proof

for x being Element of [.0,1.] holds (L[01] (((0,1) (#)),((#) (0,1)))) . x = N_CC . x

proof

let x be Element of [.0,1.]; :: thesis: (L[01] (((0,1) (#)),((#) (0,1)))) . x = N_CC . x
reconsider xx = x as Element of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
D1: (0,1) (#) = 1 by TREAL_1:def 2;
(L[01] (((0,1) (#)),((#) (0,1)))) . x = ((1 - xx) * ((0,1) (#))) + (xx * ((#) (0,1))) by TREAL_1:def 3
.= ((1 - xx) * ((0,1) (#))) + (xx * 0) by TREAL_1:def 1
.= N_CC . x by D1, FUZIMPL3:def 6 ;
hence (L[01] (((0,1) (#)),((#) (0,1)))) . x = N_CC . x ; :: thesis: verum

end;

hence L[01] (((0,1) (#)),((#) (0,1))) = N_CC by FUNCT_2:63, BORSUK_1:40, TOPMETR:20; :: thesis: verum

end;

hence N_CC is continuous by FUZIMPL3:def 7, TOPMETR:20, TREAL_1:8; :: thesis: verum