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
A5:
for x being Element of I[01] holds 1RP . x = (f +* g) . x
([#] (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; verum