A1: ( 0 is Point of I[01] & 1 / 2 is Point of I[01] & 1 / 4 is Point of I[01] & 3 / 4 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),(3 / 4).] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
reconsider C = [.(3 / 4),1.] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
reconsider D = [.(1 / 2),1.] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
reconsider E = [.(1 / 4),(1 / 2).] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
reconsider F = [.0 ,(1 / 4).] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
set T = I[01] ;
set T1 = I[01] | A;
set T2 = I[01] | B;
set T3 = I[01] | C;
set T4 = I[01] | D;
set T5 = I[01] | E;
set T6 = I[01] | F;
A2: Closed-Interval-TSpace (3 / 4),1 = I[01] | C by TOPMETR:31;
A3: Closed-Interval-TSpace (1 / 2),1 = I[01] | D by TOPMETR:31;
A4: Closed-Interval-TSpace (1 / 4),(1 / 2) = I[01] | E by TOPMETR:31;
A5: Closed-Interval-TSpace (1 / 2),(3 / 4) = I[01] | B by TOPMETR:31;
A6: Closed-Interval-TSpace 0 ,(1 / 4) = I[01] | F by TOPMETR:31;
A7: Closed-Interval-TSpace 0 ,(1 / 2) = I[01] | A by TOPMETR:31;
set f = L[01] 0 ,(1 / 2),0 ,(1 / 4);
reconsider f = L[01] 0 ,(1 / 2),0 ,(1 / 4) as continuous Function of (I[01] | A),(I[01] | F) by A6, A7, Th38;
reconsider f = f as continuous Function of (I[01] | A),I[01] by JORDAN6:4;
A8: for x being Point of (I[01] | A) holds f . x = (1 / 2) * x

proof

let x be Point of (I[01] | A); :: thesis: f . x = (1 / 2) * x
x in the carrier of (I[01] | A) ;
then x in A by PRE_TOPC:29;
then ( 0 <= x & x <= 1 / 2 ) by XXREAL_1:1;
then f . x = ((((1 / 4) - 0 ) / ((1 / 2) - 0 )) * (x - 0 )) + 0 by Th39
.= (1 / 2) * x ;
hence f . x = (1 / 2) * x ; :: thesis: verum

end;

set g = L[01] (1 / 2),(3 / 4),(1 / 4),(1 / 2);
reconsider g = L[01] (1 / 2),(3 / 4),(1 / 4),(1 / 2) as continuous Function of (I[01] | B),(I[01] | E) by A4, A5, Th38;
reconsider g = g as continuous Function of (I[01] | B),I[01] by JORDAN6:4;
A9: for x being Point of (I[01] | B) holds g . x = x - (1 / 4)

proof

let x be Point of (I[01] | B); :: thesis: g . x = x - (1 / 4)
x in the carrier of (I[01] | B) ;
then x in B by PRE_TOPC:29;
then ( 1 / 2 <= x & x <= 3 / 4 ) by XXREAL_1:1;
then g . x = ((((1 / 2) - (1 / 4)) / ((3 / 4) - (1 / 2))) * (x - (1 / 2))) + (1 / 4) by Th39
.= x - (1 / 4) ;
hence g . x = x - (1 / 4) ; :: thesis: verum

end;

set h = L[01] (3 / 4),1,(1 / 2),1;
reconsider h = L[01] (3 / 4),1,(1 / 2),1 as continuous Function of (I[01] | C),(I[01] | D) by A2, A3, Th38;
reconsider h = h as continuous Function of (I[01] | C),I[01] by JORDAN6:4;
A10: for x being Point of (I[01] | C) holds h . x = (2 * x) - 1

proof

let x be Point of (I[01] | C); :: thesis: h . x = (2 * x) - 1
x in the carrier of (I[01] | C) ;
then x in C by PRE_TOPC:29;
then ( 3 / 4 <= x & x <= 1 ) by XXREAL_1:1;
then h . x = (((1 - (1 / 2)) / (1 - (3 / 4))) * (x - (3 / 4))) + (1 / 2) by Th39
.= (2 * x) - 1 ;
hence h . x = (2 * x) - 1 ; :: thesis: verum

end;

reconsider G = [.0 ,(3 / 4).] as non empty compact Subset of I[01] by A1, BORSUK_4:49;
reconsider TT1 = I[01] | A, TT2 = I[01] | B as SubSpace of I[01] | G by TOPMETR:29, XXREAL_1:34;
set f1 = f;
set g1 = g;
A11: ([#] TT1) \/ ([#] TT2) = A \/ ([#] TT2) by PRE_TOPC:def 10
.= A \/ B by PRE_TOPC:def 10
.= [.0 ,(3 / 4).] by XXREAL_1:174
.= [#] (I[01] | G) by PRE_TOPC:def 10 ;
A13: ([#] TT1) /\ ([#] TT2) = A /\ ([#] TT2) by PRE_TOPC:def 10
.= A /\ B by PRE_TOPC:def 10
.= {(1 / 2)} by XXREAL_1:418 ;
for p being set st p in ([#] TT1) /\ ([#] TT2) holds
f . p = g . p

proof

let p be set ; :: thesis: ( p in ([#] TT1) /\ ([#] TT2) implies f . p = g . p )
assume p in ([#] TT1) /\ ([#] TT2) ; :: thesis: f . p = g . p
then A14: p = 1 / 2 by A13, TARSKI:def 1;
then reconsider p = p as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
f . p = ((((1 / 4) - 0 ) / ((1 / 2) - 0 )) * (p - 0 )) + 0 by A14, Th39
.= ((((1 / 2) - (1 / 4)) / ((3 / 4) - (1 / 2))) * (p - (1 / 2))) + (1 / 4) by A14
.= g . p by A14, Th39 ;
hence f . p = g . p ; :: thesis: verum

end;

then consider FF being Function of (I[01] | G),I[01] such that
A15: ( FF = f +* g & FF is continuous ) by A11, BORSUK_2:1;
A16: ([#] (I[01] | G)) \/ ([#] (I[01] | C)) = G \/ ([#] (I[01] | C)) by PRE_TOPC:def 10
.= G \/ C by PRE_TOPC:def 10
.= [#] I[01] by BORSUK_1:83, XXREAL_1:174 ;
A17: ([#] (I[01] | G)) /\ ([#] (I[01] | C)) = G /\ ([#] (I[01] | C)) by PRE_TOPC:def 10
.= G /\ C by PRE_TOPC:def 10
.= {(3 / 4)} by XXREAL_1:418 ;
for p being set st p in ([#] (I[01] | G)) /\ ([#] (I[01] | C)) holds
FF . p = h . p

proof

let p be set ; :: thesis: ( p in ([#] (I[01] | G)) /\ ([#] (I[01] | C)) implies FF . p = h . p )
assume p in ([#] (I[01] | G)) /\ ([#] (I[01] | C)) ; :: thesis: FF . p = h . p
then A18: p = 3 / 4 by A17, TARSKI:def 1;
then reconsider p = p as Point of I[01] by BORSUK_1:86;
p in [.(1 / 2),(3 / 4).] by A18, XXREAL_1:1;
then p in the carrier of (I[01] | B) by PRE_TOPC:29;
then p in dom g by FUNCT_2:def 1;
then FF . p = g . p by A15, FUNCT_4:14
.= 1 / 2 by A18, Th37
.= h . p by A18, Th37 ;
hence FF . p = h . p ; :: thesis: verum

end;

then consider HH being Function of I[01] ,I[01] such that
A19: ( HH = FF +* h & HH is continuous ) by A15, A16, BORSUK_2:1;
for x being Element of I[01] holds HH . x = 3RP . x

proof

let x be Element of I[01] ; :: thesis: HH . x = 3RP . x
A20: ( 0 <= x & x <= 1 ) by BORSUK_1:86;

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

suppose A21: x < 1 / 2 ; :: thesis: HH . x = 3RP . x

then x in [.0 ,(1 / 2).] by A20, XXREAL_1:1;
then A22: x is Point of (I[01] | A) by PRE_TOPC:29;
not x in [.(1 / 2),(3 / 4).] by A21, XXREAL_1:1;
then not x in the carrier of (I[01] | B) by PRE_TOPC:29;
then A23: not x in dom g ;
x < 3 / 4 by A21, XXREAL_0:2;
then not x in [.(3 / 4),1.] by XXREAL_1:1;
then not x in the carrier of (I[01] | C) by PRE_TOPC:29;
then not x in dom h ;
then HH . x = FF . x by A19, FUNCT_4:12
.= f . x by A15, A23, FUNCT_4:12
.= (1 / 2) * x by A8, A22
.= 3RP . x by A21, Def9 ;
hence HH . x = 3RP . x ; :: thesis: verum

end;

suppose A24: x = 1 / 2 ; :: thesis: HH . x = 3RP . x

then x in [.(1 / 2),(3 / 4).] by XXREAL_1:1;
then x in the carrier of (I[01] | B) by PRE_TOPC:29;
then A25: x in dom g by FUNCT_2:def 1;
not x in [.(3 / 4),1.] by A24, XXREAL_1:1;
then not x in the carrier of (I[01] | C) by PRE_TOPC:29;
then not x in dom h ;
then HH . x = FF . x by A19, FUNCT_4:12
.= g . x by A15, A25, FUNCT_4:14
.= (1 / 2) * x by A24, Th37
.= 3RP . x by A24, Def9 ;
hence HH . x = 3RP . x ; :: thesis: verum

end;

suppose A26: ( x > 1 / 2 & x < 3 / 4 ) ; :: thesis: HH . x = 3RP . x

then x in [.(1 / 2),(3 / 4).] by XXREAL_1:1;
then A27: x in the carrier of (I[01] | B) by PRE_TOPC:29;
then A28: x in dom g by FUNCT_2:def 1;
not x in [.(3 / 4),1.] by A26, XXREAL_1:1;
then not x in the carrier of (I[01] | C) by PRE_TOPC:29;
then not x in dom h ;
then HH . x = FF . x by A19, FUNCT_4:12
.= g . x by A15, A28, FUNCT_4:14
.= x - (1 / 4) by A9, A27
.= 3RP . x by A26, Def9 ;
hence HH . x = 3RP . x ; :: thesis: verum

end;

suppose A29: x = 3 / 4 ; :: thesis: HH . x = 3RP . x

then x in [.(3 / 4),1.] by XXREAL_1:1;
then x in the carrier of (I[01] | C) by PRE_TOPC:29;
then x in dom h by FUNCT_2:def 1;
then HH . x = h . x by A19, FUNCT_4:14
.= x - (1 / 4) by A29, Th37
.= 3RP . x by A29, Def9 ;
hence HH . x = 3RP . x ; :: thesis: verum

end;

suppose A30: x > 3 / 4 ; :: thesis: HH . x = 3RP . x

then x in [.(3 / 4),1.] by A20, XXREAL_1:1;
then A31: x in the carrier of (I[01] | C) by PRE_TOPC:29;
then x in dom h by FUNCT_2:def 1;
then HH . x = h . x by A19, FUNCT_4:14
.= (2 * x) - 1 by A10, A31
.= 3RP . x by A30, Def9 ;
hence HH . x = 3RP . x ; :: thesis: verum

end;

end;

end;

hence 3RP is continuous by A19, FUNCT_2:113; :: thesis: verum