let n be Element of NAT ; for w1, w2, w3 being Point of (TOP-REAL n)
for P being non empty Subset of (TOP-REAL n)
for h1, h2 being Function of I[01],((TOP-REAL n) | P) st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01],((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
let w1, w2, w3 be Point of (TOP-REAL n); for P being non empty Subset of (TOP-REAL n)
for h1, h2 being Function of I[01],((TOP-REAL n) | P) st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01],((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
let P be non empty Subset of (TOP-REAL n); for h1, h2 being Function of I[01],((TOP-REAL n) | P) st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01],((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
let h1, h2 be Function of I[01],((TOP-REAL n) | P); ( h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 implies ex h3 being Function of I[01],((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 ) )
assume that
A1:
h1 is continuous
and
A2:
w1 = h1 . 0
and
A3:
w2 = h1 . 1
and
A4:
h2 is continuous
and
A5:
w2 = h2 . 0
and
A6:
w3 = h2 . 1
; ex h3 being Function of I[01],((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
then reconsider p1 = w1, p2 = w2, p3 = w3 as Point of ((TOP-REAL n) | P) by A2, A3, A6, BORSUK_1:40, FUNCT_2:5;
p2,p3 are_connected
by A4, A5, A6, BORSUK_2:def 1;
then reconsider P2 = h2 as Path of p2,p3 by A4, A5, A6, BORSUK_2:def 2;
p1,p2 are_connected
by A1, A2, A3, BORSUK_2:def 1;
then reconsider P1 = h1 as Path of p1,p2 by A1, A2, A3, BORSUK_2:def 2;
ex P0 being Path of p1,p3 st
( P0 is continuous & P0 . 0 = p1 & P0 . 1 = p3 & ( for t being Point of I[01]
for t9 being Real st t = t9 holds
( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = P1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = P2 . ((2 * t9) - 1) ) ) ) )
proof
1
/ 2
in { r where r is Real : ( 0 <= r & r <= 1 ) }
;
then reconsider pol = 1
/ 2 as
Point of
I[01] by BORSUK_1:40, RCOMP_1:def 1;
reconsider T1 =
Closed-Interval-TSpace (
0,
(1 / 2)),
T2 =
Closed-Interval-TSpace (
(1 / 2),1) as
SubSpace of
I[01] by TOPMETR:20, TREAL_1:3;
set e2 =
P[01] (
(1 / 2),1,
((#) (0,1)),
((0,1) (#)));
set e1 =
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#)));
set E1 =
P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))));
set E2 =
P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))));
set f =
(P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))));
A7:
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) =
the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by FUNCT_2:def 1
.=
[.0,(1 / 2).]
by TOPMETR:18
;
A8:
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) =
the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by FUNCT_2:def 1
.=
[.(1 / 2),1.]
by TOPMETR:18
;
reconsider gg =
P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as
Function of
T2,
((TOP-REAL n) | P) by TOPMETR:20;
reconsider ff =
P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as
Function of
T1,
((TOP-REAL n) | P) by TOPMETR:20;
A9:
for
t9 being
Real st 1
/ 2
<= t9 &
t9 <= 1 holds
(P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = P2 . ((2 * t9) - 1)
proof
reconsider r1 =
(#) (
0,1),
r2 = (
0,1)
(#) as
Real by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5;
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by FUNCT_2:def 1;
then A10:
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) =
[.(1 / 2),1.]
by TOPMETR:18
.=
{ r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
by RCOMP_1:def 1
;
let t9 be
Real;
( 1 / 2 <= t9 & t9 <= 1 implies (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = P2 . ((2 * t9) - 1) )
assume
( 1
/ 2
<= t9 &
t9 <= 1 )
;
(P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = P2 . ((2 * t9) - 1)
then A11:
t9 in dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))
by A10;
then reconsider s =
t9 as
Point of
(Closed-Interval-TSpace ((1 / 2),1)) ;
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . s =
(((r2 - r1) / (1 - (1 / 2))) * t9) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2)))
by TREAL_1:11
.=
(2 * t9) - 1
by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5
;
hence
(P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = P2 . ((2 * t9) - 1)
by A11, FUNCT_1:13;
verum
end;
A12:
for
t9 being
Real st
0 <= t9 &
t9 <= 1
/ 2 holds
(P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P1 . (2 * t9)
proof
reconsider r1 =
(#) (
0,1),
r2 = (
0,1)
(#) as
Real by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5;
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by FUNCT_2:def 1;
then A13:
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) =
[.0,(1 / 2).]
by TOPMETR:18
.=
{ r where r is Real : ( 0 <= r & r <= 1 / 2 ) }
by RCOMP_1:def 1
;
let t9 be
Real;
( 0 <= t9 & t9 <= 1 / 2 implies (P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P1 . (2 * t9) )
assume
(
0 <= t9 &
t9 <= 1
/ 2 )
;
(P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P1 . (2 * t9)
then A14:
t9 in dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))
by A13;
then reconsider s =
t9 as
Point of
(Closed-Interval-TSpace (0,(1 / 2))) ;
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . s =
(((r2 - r1) / ((1 / 2) - 0)) * t9) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0))
by TREAL_1:11
.=
2
* t9
by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5
;
hence
(P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P1 . (2 * t9)
by A14, FUNCT_1:13;
verum
end;
then A15:
ff . (1 / 2) =
P2 . ((2 * (1 / 2)) - 1)
by A3, A5
.=
gg . pol
by A9
;
(
[#] T1 = [.0,(1 / 2).] &
[#] T2 = [.(1 / 2),1.] )
by TOPMETR:18;
then A16:
(
([#] T1) \/ ([#] T2) = [#] I[01] &
([#] T1) /\ ([#] T2) = {pol} )
by BORSUK_1:40, XXREAL_1:174, XXREAL_1:418;
rng ((P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= (rng (P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))))
by FUNCT_4:17;
then A17:
rng ((P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= the
carrier of
((TOP-REAL n) | P)
by XBOOLE_1:1;
A18:
(
T1 is
compact &
T2 is
compact )
by HEINE:4;
dom P1 = the
carrier of
I[01]
by FUNCT_2:def 1;
then A19:
rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) c= dom P1
by TOPMETR:20;
(
dom P2 = the
carrier of
I[01] &
rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) c= the
carrier of
(Closed-Interval-TSpace (0,1)) )
by FUNCT_2:def 1;
then A20:
dom (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) = dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))
by RELAT_1:27, TOPMETR:20;
not
0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
proof
assume
0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
contradiction
then
ex
rr being
Real st
(
rr = 0 & 1
/ 2
<= rr &
rr <= 1 )
;
hence
contradiction
;
verum
end;
then
not
0 in dom (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
by A8, A20, RCOMP_1:def 1;
then A21:
((P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 =
(P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0
by FUNCT_4:11
.=
P1 . (2 * 0)
by A12
.=
p1
by A2
;
dom ((P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) =
(dom (P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))))
by FUNCT_4:def 1
.=
[.0,(1 / 2).] \/ [.(1 / 2),1.]
by A7, A8, A19, A20, RELAT_1:27
.=
the
carrier of
I[01]
by BORSUK_1:40, XXREAL_1:174
;
then reconsider f =
(P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) as
Function of
I[01],
((TOP-REAL n) | P) by A17, FUNCT_2:def 1, RELSET_1:4;
(
P[01] (
0,
(1 / 2),
((#) (0,1)),
((0,1) (#))) is
continuous &
P[01] (
(1 / 2),1,
((#) (0,1)),
((0,1) (#))) is
continuous )
by TREAL_1:12;
then reconsider f =
f as
continuous Function of
I[01],
((TOP-REAL n) | P) by A1, A4, A15, A16, A18, COMPTS_1:20, TOPMETR:20;
1
in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
then
1
in dom (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
by A8, A20, RCOMP_1:def 1;
then A22:
f . 1 =
(P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1
by FUNCT_4:13
.=
P2 . ((2 * 1) - 1)
by A9
.=
p3
by A6
;
then
p1,
p3 are_connected
by A21, BORSUK_2:def 1;
then reconsider f =
f as
Path of
p1,
p3 by A21, A22, BORSUK_2:def 2;
for
t being
Point of
I[01] for
t9 being
Real st
t = t9 holds
( (
0 <= t9 &
t9 <= 1
/ 2 implies
f . t = P1 . (2 * t9) ) & ( 1
/ 2
<= t9 &
t9 <= 1 implies
f . t = P2 . ((2 * t9) - 1) ) )
proof
let t be
Point of
I[01];
for t9 being Real st t = t9 holds
( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = P1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = P2 . ((2 * t9) - 1) ) )let t9 be
Real;
( t = t9 implies ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = P1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = P2 . ((2 * t9) - 1) ) ) )
assume A23:
t = t9
;
( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = P1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = P2 . ((2 * t9) - 1) ) )
thus
(
0 <= t9 &
t9 <= 1
/ 2 implies
f . t = P1 . (2 * t9) )
( 1 / 2 <= t9 & t9 <= 1 implies f . t = P2 . ((2 * t9) - 1) )proof
assume A24:
(
0 <= t9 &
t9 <= 1
/ 2 )
;
f . t = P1 . (2 * t9)
then
t9 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) }
;
then A25:
t9 in [.0,(1 / 2).]
by RCOMP_1:def 1;
per cases
( t9 <> 1 / 2 or t9 = 1 / 2 )
;
suppose A26:
t9 <> 1
/ 2
;
f . t = P1 . (2 * t9)
not
t9 in dom (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
proof
assume
t9 in dom (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
;
contradiction
then
t9 in [.0,(1 / 2).] /\ [.(1 / 2),1.]
by A8, A20, A25, XBOOLE_0:def 4;
then
t9 in {(1 / 2)}
by XXREAL_1:418;
hence
contradiction
by A26, TARSKI:def 1;
verum
end; then f . t =
(P1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t
by A23, FUNCT_4:11
.=
P1 . (2 * t9)
by A12, A23, A24
;
hence
f . t = P1 . (2 * t9)
;
verum suppose A27:
t9 = 1
/ 2
;
f . t = P1 . (2 * t9)
1
/ 2
in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
then
1
/ 2
in [.(1 / 2),1.]
by RCOMP_1:def 1;
then
1
/ 2
in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
t in dom (P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
by A23, A27, FUNCT_2:def 1, TOPMETR:20;
then f . t =
(P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . (1 / 2)
by A23, A27, FUNCT_4:13
.=
P1 . (2 * t9)
by A12, A15, A27
;
hence
f . t = P1 . (2 * t9)
;
verum
end;
thus
( 1
/ 2
<= t9 &
t9 <= 1 implies
f . t = P2 . ((2 * t9) - 1) )
verumproof
assume A28:
( 1
/ 2
<= t9 &
t9 <= 1 )
;
f . t = P2 . ((2 * t9) - 1)
then
t9 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
then
t9 in [.(1 / 2),1.]
by RCOMP_1:def 1;
then f . t =
(P2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t
by A8, A20, A23, FUNCT_4:13
.=
P2 . ((2 * t9) - 1)
by A9, A23, A28
;
hence
f . t = P2 . ((2 * t9) - 1)
;
verum
end;
end;
hence
ex
P0 being
Path of
p1,
p3 st
(
P0 is
continuous &
P0 . 0 = p1 &
P0 . 1
= p3 & ( for
t being
Point of
I[01] for
t9 being
Real st
t = t9 holds
( (
0 <= t9 &
t9 <= 1
/ 2 implies
P0 . t = P1 . (2 * t9) ) & ( 1
/ 2
<= t9 &
t9 <= 1 implies
P0 . t = P2 . ((2 * t9) - 1) ) ) ) )
by A21, A22;
verum
end;
hence
ex h3 being Function of I[01],((TOP-REAL n) | P) st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 )
; verum