A1:
1 / 2 is Point of I[01]
by BORSUK_1:43;
A2:
3 / 4 is Point of I[01]
by BORSUK_1:43;
then reconsider B = [.(1 / 2),(3 / 4).] as non empty compact Subset of I[01] by A1, BORSUK_4:24;
A3:
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;
reconsider G = [.0,(3 / 4).] as non empty compact Subset of I[01] by A3, A2, BORSUK_4:24;
A4:
1 / 4 is Point of I[01]
by BORSUK_1:43;
then reconsider E = [.(1 / 4),(1 / 2).] as non empty compact Subset of I[01] by A1, BORSUK_4:24;
reconsider F = [.0,(1 / 4).] as non empty compact Subset of I[01] by A3, A4, BORSUK_4:24;
A5:
1 is Point of I[01]
by BORSUK_1:43;
then reconsider C = [.(3 / 4),1.] as non empty compact Subset of I[01] by A2, BORSUK_4:24;
reconsider D = [.(1 / 2),1.] as non empty compact Subset of I[01] by A1, A5, BORSUK_4:24;
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;
set f = L[01] (0,(1 / 2),0,(1 / 4));
set g = L[01] ((1 / 2),(3 / 4),(1 / 4),(1 / 2));
set h = L[01] ((3 / 4),1,(1 / 2),1);
reconsider TT1 = I[01] | A, TT2 = I[01] | B as SubSpace of I[01] | G by TOPMETR:22, XXREAL_1:34;
( Closed-Interval-TSpace ((3 / 4),1) = I[01] | C & Closed-Interval-TSpace ((1 / 2),1) = I[01] | D )
by TOPMETR:24;
then reconsider h = L[01] ((3 / 4),1,(1 / 2),1) as continuous Function of (I[01] | C),(I[01] | D) by Th34;
reconsider h = h as continuous Function of (I[01] | C),I[01] by JORDAN6:3;
A6:
for x being Point of (I[01] | C) holds h . x = (2 * x) - 1
( Closed-Interval-TSpace (0,(1 / 4)) = I[01] | F & Closed-Interval-TSpace (0,(1 / 2)) = I[01] | A )
by TOPMETR:24;
then reconsider f = L[01] (0,(1 / 2),0,(1 / 4)) as continuous Function of (I[01] | A),(I[01] | F) by Th34;
( Closed-Interval-TSpace ((1 / 4),(1 / 2)) = I[01] | E & Closed-Interval-TSpace ((1 / 2),(3 / 4)) = I[01] | B )
by TOPMETR:24;
then reconsider g = L[01] ((1 / 2),(3 / 4),(1 / 4),(1 / 2)) as continuous Function of (I[01] | B),(I[01] | E) by Th34;
reconsider g = g as continuous Function of (I[01] | B),I[01] by JORDAN6:3;
reconsider f = f as continuous Function of (I[01] | A),I[01] by JORDAN6:3;
set f1 = f;
set g1 = g;
A7:
for x being Point of (I[01] | B) holds g . x = x - (1 / 4)
A8: ([#] TT1) /\ ([#] TT2) =
A /\ ([#] TT2)
by PRE_TOPC:def 5
.=
A /\ B
by PRE_TOPC:def 5
.=
{(1 / 2)}
by XXREAL_1:418
;
A9:
for p being set st p in ([#] TT1) /\ ([#] TT2) holds
f . p = g . p
([#] TT1) \/ ([#] TT2) =
A \/ ([#] TT2)
by PRE_TOPC:def 5
.=
A \/ B
by PRE_TOPC:def 5
.=
[.0,(3 / 4).]
by XXREAL_1:174
.=
[#] (I[01] | G)
by PRE_TOPC:def 5
;
then consider FF being Function of (I[01] | G),I[01] such that
A11:
FF = f +* g
and
A12:
FF is continuous
by A9, BORSUK_2:1;
A13: ([#] (I[01] | G)) /\ ([#] (I[01] | C)) =
G /\ ([#] (I[01] | C))
by PRE_TOPC:def 5
.=
G /\ C
by PRE_TOPC:def 5
.=
{(3 / 4)}
by XXREAL_1:418
;
A14:
for p being set st p in ([#] (I[01] | G)) /\ ([#] (I[01] | C)) holds
FF . p = h . p
([#] (I[01] | G)) \/ ([#] (I[01] | C)) =
G \/ ([#] (I[01] | C))
by PRE_TOPC:def 5
.=
G \/ C
by PRE_TOPC:def 5
.=
[#] I[01]
by BORSUK_1:40, XXREAL_1:174
;
then consider HH being Function of I[01],I[01] such that
A16:
HH = FF +* h
and
A17:
HH is continuous
by A12, A14, BORSUK_2:1;
A18:
for x being Point of (I[01] | A) holds f . x = (1 / 2) * x
for x being Element of I[01] holds HH . x = 3RP . x
proof
let x be
Element of
I[01];
HH . x = 3RP . x
A19:
0 <= x
by BORSUK_1:43;
A20:
x <= 1
by BORSUK_1:43;
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
;
HH . x = 3RP . xthen
not
x in [.(1 / 2),(3 / 4).]
by XXREAL_1:1;
then
not
x in the
carrier of
(I[01] | B)
by PRE_TOPC:8;
then A22:
not
x in dom g
;
x in [.0,(1 / 2).]
by A19, A21, XXREAL_1:1;
then A23:
x is
Point of
(I[01] | A)
by PRE_TOPC:8;
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:8;
then
not
x in dom h
;
then HH . x =
FF . x
by A16, FUNCT_4:11
.=
f . x
by A11, A22, FUNCT_4:11
.=
(1 / 2) * x
by A18, A23
.=
3RP . x
by A21, Def7
;
hence
HH . x = 3RP . x
;
verum end;
end;
hence
3RP is continuous
by A17, FUNCT_2:63; verum