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] | A = Closed-Interval-TSpace 0 ,(1 / 2) by TOPMETR:31;
then reconsider f = L[01] 0 ,(1 / 2),0 ,1 as continuous Function of (I[01] | A),I[01] by Th38, TOPMETR:27;
reconsider g = (I[01] | B) --> 1[01] as continuous Function of (I[01] | B),I[01] ;
A2: g = the carrier of (I[01] | B) --> 1 by BORSUK_1:def 18;
A3: ([#] (I[01] | A)) \/ ([#] (I[01] | B)) = [.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] | A)) /\ ([#] (I[01] | B)) holds
f . p = g . p

proof

let p be set ; :: thesis: ( p in ([#] (I[01] | A)) /\ ([#] (I[01] | B)) implies f . p = g . p )
assume p in ([#] (I[01] | A)) /\ ([#] (I[01] | B)) ; :: 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 [.(1 / 2),1.] by XXREAL_1:1;
then A5: p in the carrier of (I[01] | B) by PRE_TOPC:29;
f . p = (((1 - 0 ) / ((1 / 2) - 0 )) * ((1 / 2) - 0 )) + 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 = f +* g & h is continuous ) by A3, BORSUK_2:1;
1RP = h

proof

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

proof

let x be Element of I[01] ; :: thesis: 1RP . x = (f +* g) . x
A7: dom g = 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: 1RP . x = (f +* g) . x

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

end;

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

then A12: x in dom g by A7, XXREAL_1:1;
thus 1RP . x = 2 * (1 / 2) by A11, Def7
.= g . x by A2, A12, FUNCOP_1:13
.= (f +* g) . x by A12, FUNCT_4:14 ; :: thesis: verum

end;

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

x <= 1 by BORSUK_1:86;
then A14: x in dom g by A7, A13, XXREAL_1:1;
thus 1RP . x = 1 by A13, Def7
.= g . x by A2, A14, FUNCOP_1:13
.= (f +* g) . x by A14, FUNCT_4:14 ; :: thesis: verum

end;

end;

end;

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

end;

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