A1: ( 0 is Point of I[01] & 1 / 2 is Point of I[01] & 1 is Point of I[01] ) by BORSUK_1:86;
then reconsider A = [.0 ,(1 / 2).] as non empty compact Subset of I[01] by BORSUK_4:49;
reconsider B = [.(1 / 2),1.] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
set T1 = I[01] | A;
set T2 = I[01] | B;
set T = I[01] ;
I[01] | B = Closed-Interval-TSpace (1 / 2),1 by TOPMETR:31;
then reconsider f = L[01] (1 / 2),1,0 ,1 as continuous Function of (I[01] | B),I[01] by Th38, TOPMETR:27;
reconsider g = (I[01] | A) --> 0[01] as continuous Function of (I[01] | A),I[01] ;
A2: g = the carrier of (I[01] | A) --> 0 by BORSUK_1:def 17;
A3: ([#] (I[01] | B)) \/ ([#] (I[01] | A)) = [.0 ,(1 / 2).] \/ ([#] (I[01] | B)) by PRE_TOPC:def 10
.= [.0 ,(1 / 2).] \/ [.(1 / 2),1.] by PRE_TOPC:def 10
.= [#] I[01] by BORSUK_1:83, XXREAL_1:174 ;
for p being set st p in ([#] (I[01] | B)) /\ ([#] (I[01] | A)) holds
f . p = g . p

proof

let p be set ; :: thesis: ( p in ([#] (I[01] | B)) /\ ([#] (I[01] | A)) implies f . p = g . p )
assume p in ([#] (I[01] | B)) /\ ([#] (I[01] | A)) ; :: thesis: f . p = g . p
then p in [.0 ,(1 / 2).] /\ ([#] (I[01] | B)) by PRE_TOPC:def 10;
then p in [.0 ,(1 / 2).] /\ [.(1 / 2),1.] by PRE_TOPC:def 10;
then p in {(1 / 2)} by XXREAL_1:418;
then A4: p = 1 / 2 by TARSKI:def 1;
then p in [.0 ,(1 / 2).] by XXREAL_1:1;
then A5: p in the carrier of (I[01] | A) by PRE_TOPC:29;
f . p = (((1 - 0 ) / (1 - (1 / 2))) * ((1 / 2) - (1 / 2))) + 0 by A4, Th39
.= g . p by A2, A5, FUNCOP_1:13 ;
hence f . p = g . p ; :: thesis: verum

end;

then consider h being Function of I[01] ,I[01] such that
A6: ( h = g +* f & h is continuous ) by A3, BORSUK_2:1;
2RP = h

proof

for x being Element of I[01] holds 2RP . x = (g +* f) . x

proof

let x be Element of I[01] ; :: thesis: 2RP . x = (g +* f) . x
A7: dom f = the carrier of (I[01] | B) by FUNCT_2:def 1
.= [.(1 / 2),1.] by PRE_TOPC:29 ;

per cases ( x > 1 / 2 or x = 1 / 2 or x < 1 / 2 ) by XXREAL_0:1;

suppose A8: x > 1 / 2 ; :: thesis: 2RP . x = (g +* f) . x

x <= 1 by BORSUK_1:86;
then A9: x in dom f by A7, A8, XXREAL_1:1;
1 >= x by BORSUK_1:86;
then A10: f . x = (((1 - 0 ) / (1 - (1 / 2))) * (x - (1 / 2))) + 0 by A8, Th39
.= (2 * x) - 1 ;
thus 2RP . x = (2 * x) - 1 by A8, Def8
.= (g +* f) . x by A9, A10, FUNCT_4:14 ; :: thesis: verum

end;

suppose A11: x = 1 / 2 ; :: thesis: 2RP . x = (g +* f) . x

then A12: x in dom f by A7, XXREAL_1:1;
thus 2RP . x = (((1 - 0 ) / (1 - (1 / 2))) * ((1 / 2) - (1 / 2))) + 0 by A11, Def8
.= f . x by A11, Th39
.= (g +* f) . x by A12, FUNCT_4:14 ; :: thesis: verum

end;

suppose A13: x < 1 / 2 ; :: thesis: 2RP . x = (g +* f) . x

then A14: not x in dom f by A7, XXREAL_1:1;
x >= 0 by BORSUK_1:86;
then x in [.0 ,(1 / 2).] by A13, XXREAL_1:1;
then A15: x in the carrier of (I[01] | A) by PRE_TOPC:29;
thus 2RP . x = 0 by A13, Def8
.= g . x by A2, A15, FUNCOP_1:13
.= (g +* f) . x by A14, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

hence 2RP = h by A6, FUNCT_2:113; :: thesis: verum

end;

hence 2RP is continuous by A6; :: thesis: verum