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:83, FUNCT_2:7;
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:83, 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:27, TREAL_1:6;
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:25
;
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:25
;
reconsider gg =
P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) as
Function of
T2,
((TOP-REAL n) | P) by TOPMETR:27;
reconsider ff =
P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) as
Function of
T1,
((TOP-REAL n) | P) by TOPMETR:27;
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 17, BORSUK_1:def 18, TREAL_1:8;
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:25
.=
{ 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:14
.=
(2 * t9) - 1
by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8
;
hence
(P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t9 = P2 . ((2 * t9) - 1)
by A11, FUNCT_1:23;
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 17, BORSUK_1:def 18, TREAL_1:8;
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:25
.=
{ 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:14
.=
2
* t9
by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8
;
hence
(P1 * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t9 = P1 . (2 * t9)
by A14, FUNCT_1:23;
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:25;
then A16:
(
([#] T1) \/ ([#] T2) = [#] I[01] &
([#] T1) /\ ([#] T2) = {pol} )
by BORSUK_1:83, 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:18;
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:11;
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:27;
(
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:46, TOPMETR:27;
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:12
.=
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:46
.=
the
carrier of
I[01]
by BORSUK_1:83, 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:11;
(
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:15;
then reconsider f =
f as
continuous Function of
I[01] ,
((TOP-REAL n) | P) by A1, A4, A15, A16, A18, COMPTS_1:29, TOPMETR:27;
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:14
.=
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:12
.=
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:25;
then
t in dom (P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
by A23, A27, FUNCT_2:def 1, TOPMETR:27;
then f . t =
(P2 * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . (1 / 2)
by A23, A27, FUNCT_4:14
.=
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:14
.=
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