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 = P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ));
set E2 = Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ));
set f = (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )));
A3: 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
;
A4: 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
;
A5:
for t9 being Real st 1 / 2 <= t9 & t9 <= 1 holds
(Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t9 = Q . ((2 * t9) - 1)
proof
reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by 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 A6:
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 (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t9 = Q . ((2 * t9) - 1) )
assume
( 1
/ 2
<= t9 &
t9 <= 1 )
;
(Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t9 = Q . ((2 * t9) - 1)
then A7:
t9 in dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))
by A6;
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 TREAL_1:8
;
hence
(Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t9 = Q . ((2 * t9) - 1)
by A7, FUNCT_1:23;
verum
end;
reconsider gg = Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) as Function of T2,T by TOPMETR:27;
reconsider ff = P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) as Function of T1,T by TOPMETR:27;
A8:
( P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ) is continuous Function of (Closed-Interval-TSpace 0 ,(1 / 2)),(Closed-Interval-TSpace 0 ,1) & P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ) is continuous )
by TREAL_1:15;
rng ((P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) c= (rng (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )))) \/ (rng (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))))
by FUNCT_4:18;
then A9:
rng ((P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) c= the carrier of T
by XBOOLE_1:1;
A10:
( R^1 is T_2 & T1 is compact )
by HEINE:11, PCOMPS_1:38, TOPMETR:def 7;
A11:
for t9 being Real st 0 <= t9 & t9 <= 1 / 2 holds
(P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t9 = P . (2 * t9)
proof
reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by 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 A12:
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 (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t9 = P . (2 * t9) )
assume
(
0 <= t9 &
t9 <= 1
/ 2 )
;
(P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t9 = P . (2 * t9)
then A13:
t9 in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))
by A12;
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))
by TREAL_1:14
.=
2
* t9
by TREAL_1:8
;
hence
(P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t9 = P . (2 * t9)
by A13, FUNCT_1:23;
verum
end;
then A14: ff . (1 / 2) =
P . (2 * (1 / 2))
.=
b
by A1, Def2
.=
Q . ((2 * (1 / 2)) - 1)
by A2, Def2
.=
gg . pol
by A5
;
dom P = the carrier of I[01]
by FUNCT_2:def 1;
then A15:
rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) c= dom P
by TOPMETR:27;
( dom Q = 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 A16:
dom (Q * (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 (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
by A4, A16, RCOMP_1:def 1;
then A17: ((P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) . 0 =
(P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . 0
by FUNCT_4:12
.=
P . (2 * 0 )
by A11
.=
a
by A1, Def2
;
A18: dom ((P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))) =
(dom (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )))) \/ (dom (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))))
by FUNCT_4:def 1
.=
[.0 ,(1 / 2).] \/ [.(1 / 2),1.]
by A3, A4, A15, A16, RELAT_1:46
.=
the carrier of I[01]
by BORSUK_1:83, XXREAL_1:174
;
( [#] T1 = [.0 ,(1 / 2).] & [#] T2 = [.(1 / 2),1.] )
by TOPMETR:25;
then A19:
( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} )
by BORSUK_1:83, XXREAL_1:174, XXREAL_1:418;
A20:
T2 is compact
by HEINE:11;
reconsider f = (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) +* (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) as Function of I[01] ,T by A18, A9, FUNCT_2:def 1, RELSET_1:11;
( P is continuous & Q is continuous )
by A1, A2, Def2;
then reconsider f = f as continuous Function of I[01] ,T by A8, A14, A19, A10, A20, COMPTS_1:29, TOPMETR:27;
1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
;
then
1 in dom (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
by A4, A16, RCOMP_1:def 1;
then A21: f . 1 =
(Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . 1
by FUNCT_4:14
.=
Q . ((2 * 1) - 1)
by A5
.=
c
by A2, Def2
;
then
a,c are_connected
by A17, Def1;
then reconsider f = f as Path of a,c by A17, A21, Def2;
for t being Point of I[01] holds
( ( t <= 1 / 2 implies f . t = P . (2 * t) ) & ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) )
proof
let t be
Point of
I[01] ;
( ( t <= 1 / 2 implies f . t = P . (2 * t) ) & ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) )
A22:
t is
Real
by XREAL_0:def 1;
A23:
0 <= t
by Lm1;
thus
(
t <= 1
/ 2 implies
f . t = P . (2 * t) )
( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) )proof
assume A24:
t <= 1
/ 2
;
f . t = P . (2 * t)
then
t in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) }
by A23, A22;
then A25:
t in [.0 ,(1 / 2).]
by RCOMP_1:def 1;
per cases
( t <> 1 / 2 or t = 1 / 2 )
;
suppose A26:
t <> 1
/ 2
;
f . t = P . (2 * t)
not
t in dom (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
proof
assume
t in dom (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
;
contradiction
then
t in [.0 ,(1 / 2).] /\ [.(1 / 2),1.]
by A4, A16, A25, XBOOLE_0:def 4;
then
t in {(1 / 2)}
by XXREAL_1:418;
hence
contradiction
by A26, TARSKI:def 1;
verum
end; then f . t =
(P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t
by FUNCT_4:12
.=
P . (2 * t)
by A11, A23, A22, A24
;
hence
f . t = P . (2 * t)
;
verum suppose A27:
t = 1
/ 2
;
f . t = P . (2 * t)
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 (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )))
by A27, FUNCT_2:def 1, TOPMETR:27;
then f . t =
(P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t
by A14, A27, FUNCT_4:14
.=
P . (2 * t)
by A11, A23, A22, A24
;
hence
f . t = P . (2 * t)
;
verum
end;
A28:
t <= 1
by Lm1;
thus
( 1
/ 2
<= t implies
f . t = Q . ((2 * t) - 1) )
verumproof
assume A29:
1
/ 2
<= t
;
f . t = Q . ((2 * t) - 1)
then
t in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
by A28, A22;
then
t in [.(1 / 2),1.]
by RCOMP_1:def 1;
then f . t =
(Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t
by A4, A16, FUNCT_4:14
.=
Q . ((2 * t) - 1)
by A5, A28, A22, A29
;
hence
f . t = Q . ((2 * t) - 1)
;
verum
end;
end;
hence
ex b1 being Path of a,c st
for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) )
; verum