A1: 1 / 2 is Point of I[01] by BORSUK_1:86;
1 is Point of I[01] by BORSUK_1:86;
then reconsider B = [.(1 / 2),1.] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
0 is Point of I[01] by BORSUK_1:86;
then reconsider A = [.0 ,(1 / 2).] 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] ;
reconsider g = (I[01] | A) --> 0[01] as continuous Function of (I[01] | A),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;
A2: 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 A3: p = 1 / 2 by TARSKI:def 1;
then p in [.0 ,(1 / 2).] by XXREAL_1:1;
then A4: 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 A3, Th39
.= g . p by A4, BORSUK_1:def 17, FUNCOP_1:13 ;
hence f . p = g . p ; :: thesis: verum

end;

A5: 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
A6: 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 A7: x > 1 / 2 ; :: thesis: 2RP . x = (g +* f) . x

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

end;

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

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

end;

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

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

end;

end;

end;

([#] (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 ;
then ex h being Function of I[01] ,I[01] st
( h = g +* f & h is continuous ) by A2, BORSUK_2:1;
hence 2RP is continuous by A5, FUNCT_2:113; :: thesis: verum