A1: 1 / 2 is Point of I[01] by BORSUK_1:43;
1 is Point of I[01] by BORSUK_1:43;
then reconsider B = [.(1 / 2),1.] as non empty compact Subset of I[01] by A1, BORSUK_4:24;
0 is Point of I[01] by BORSUK_1:43;
then reconsider A = [.0,(1 / 2).] as non empty compact Subset of I[01] by A1, BORSUK_4:24;
set T1 = I[01] | A;
set T2 = I[01] | B;
set T = I[01] ;
reconsider g = (I[01] | B) --> 1[01] as continuous Function of (I[01] | B),I[01] ;
I[01] | A = Closed-Interval-TSpace (0,(1 / 2)) by TOPMETR:24;
then reconsider f = L[01] (0,(1 / 2),0,1) as continuous Function of (I[01] | A),I[01] by Th34, TOPMETR:20;
A2: 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 5;
then p in [.0,(1 / 2).] /\ [.(1 / 2),1.] by PRE_TOPC:def 5;
then p in {(1 / 2)} by XXREAL_1:418;
then A3: p = 1 / 2 by TARSKI:def 1;
then p in [.(1 / 2),1.] by XXREAL_1:1;
then A4: p in the carrier of (I[01] | B) by PRE_TOPC:8;
f . p = (((1 - 0) / ((1 / 2) - 0)) * ((1 / 2) - 0)) + 0 by A3, Th35
.= g . p by A4, BORSUK_1:def 15, FUNCOP_1:7 ;
hence f . p = g . p ; :: thesis: verum

end;

A5: 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
A6: dom g = the carrier of (I[01] | B) by FUNCT_2:def 1
.= [.(1 / 2),1.] by PRE_TOPC:8 ;

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

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

0 <= x by BORSUK_1:43;
then A8: f . x = (((1 - 0) / ((1 / 2) - 0)) * (x - 0)) + 0 by A7, Th35
.= (1 / (1 / 2)) * x ;
A9: not x in dom g by A6, A7, XXREAL_1:1;
thus 1RP . x = 2 * x by A7, Def5
.= (f +* g) . x by A9, A8, FUNCT_4:11 ; :: thesis: verum

end;

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

then A11: x in dom g by A6, XXREAL_1:1;
thus 1RP . x = 2 * (1 / 2) by A10, Def5
.= g . x by A11, BORSUK_1:def 15, FUNCOP_1:7
.= (f +* g) . x by A11, FUNCT_4:13 ; :: thesis: verum

end;

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

x <= 1 by BORSUK_1:43;
then A13: x in dom g by A6, A12, XXREAL_1:1;
thus 1RP . x = 1 by A12, Def5
.= g . x by A13, BORSUK_1:def 15, FUNCOP_1:7
.= (f +* g) . x by A13, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

([#] (I[01] | A)) \/ ([#] (I[01] | B)) = [.0,(1 / 2).] \/ ([#] (I[01] | B)) by PRE_TOPC:def 5
.= [.0,(1 / 2).] \/ [.(1 / 2),1.] by PRE_TOPC:def 5
.= [#] I[01] by BORSUK_1:40, XXREAL_1:174 ;
then ex h being Function of I[01],I[01] st
( h = f +* g & h is continuous ) by A2, BORSUK_2:1;
hence 1RP is continuous by A5, FUNCT_2:63; :: thesis: verum