let G be non empty TopSpace; :: thesis: for w1, w2, w3 being Point of G

for h1, h2 being Function of I[01],G 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],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )

let w1, w2, w3 be Point of G; :: thesis: for h1, h2 being Function of I[01],G 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],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )

let h1, h2 be Function of I[01],G; :: thesis: ( 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],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) )

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 ; :: thesis: ex h3 being Function of I[01],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )

w2,w3 are_connected by A4, A5, A6;

then reconsider g2 = h2 as Path of w2,w3 by A4, A5, A6, Def2;

w1,w2 are_connected by A1, A2, A3;

then reconsider g1 = h1 as Path of w1,w2 by A1, A2, A3, Def2;

set P1 = g1;

set P2 = g2;

set p1 = w1;

set p3 = w3;

ex P0 being Path of w1,w3 st

( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) )

A31: ( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 ) and

A32: for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ;

rng P0 c= (rng g1) \/ (rng g2)

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) by A31; :: thesis: verum

for h1, h2 being Function of I[01],G 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],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )

let w1, w2, w3 be Point of G; :: thesis: for h1, h2 being Function of I[01],G 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],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )

let h1, h2 be Function of I[01],G; :: thesis: ( 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],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) )

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 ; :: thesis: ex h3 being Function of I[01],G st

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )

w2,w3 are_connected by A4, A5, A6;

then reconsider g2 = h2 as Path of w2,w3 by A4, A5, A6, Def2;

w1,w2 are_connected by A1, A2, A3;

then reconsider g1 = h1 as Path of w1,w2 by A1, A2, A3, Def2;

set P1 = g1;

set P2 = g2;

set p1 = w1;

set p3 = w3;

ex P0 being Path of w1,w3 st

( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) )

proof

then consider P0 being Path of w1,w3 such that
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 = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))));

set E2 = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))));

set f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (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 = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of T2,G by TOPMETR:20;

reconsider ff = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of T1,G by TOPMETR:20;

A9: for t9 being Real st 1 / 2 <= t9 & t9 <= 1 holds

(g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1)

(g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9)

.= 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;

A17: T2 is compact by HEINE:4;

dom g1 = the carrier of I[01] by FUNCT_2:def 1;

then A18: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) c= dom g1 by TOPMETR:20;

( dom g2 = 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 A19: dom (g2 * (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 ) }

then A20: ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 by FUNCT_4:11

.= g1 . (2 * 0) by A12

.= w1 by A2 ;

A21: dom ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) = (dom (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:def 1

.= [.0,(1 / 2).] \/ [.(1 / 2),1.] by A7, A8, A18, A19, RELAT_1:27

.= the carrier of I[01] by BORSUK_1:40, XXREAL_1:174 ;

rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= (rng (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:17;

then A22: rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= the carrier of G by XBOOLE_1:1;

A23: ( R^1 is T_2 & T1 is compact ) by HEINE:4, PCOMPS_1:34, TOPMETR:def 6;

reconsider f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) as Function of I[01],G by A21, A22, 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],G by A1, A4, A15, A16, A23, A17, COMPTS_1:20, TOPMETR:20;

1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;

then 1 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A8, A19, RCOMP_1:def 1;

then A24: f . 1 = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 by FUNCT_4:13

.= g2 . ((2 * 1) - 1) by A9

.= w3 by A6 ;

then w1,w3 are_connected by A20;

then reconsider f = f as Path of w1,w3 by A20, A24, Def2;

for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )

( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) ) by A20, A24; :: thesis: verum

end;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 = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))));

set E2 = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))));

set f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (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 = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of T2,G by TOPMETR:20;

reconsider ff = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of T1,G by TOPMETR:20;

A9: for t9 being Real st 1 / 2 <= t9 & t9 <= 1 holds

(g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1)

proof

A12:
for t9 being Real st 0 <= t9 & t9 <= 1 / 2 holds
reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real ;

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; :: thesis: ( 1 / 2 <= t9 & t9 <= 1 implies (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) )

assume ( 1 / 2 <= t9 & t9 <= 1 ) ; :: thesis: (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((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 TREAL_1:5 ;

hence (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) by A11, FUNCT_1:13; :: thesis: verum

end;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; :: thesis: ( 1 / 2 <= t9 & t9 <= 1 implies (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) )

assume ( 1 / 2 <= t9 & t9 <= 1 ) ; :: thesis: (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((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 TREAL_1:5 ;

hence (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) by A11, FUNCT_1:13; :: thesis: verum

(g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9)

proof

then A15: ff . (1 / 2) =
g2 . ((2 * (1 / 2)) - 1)
by A3, A5
reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real ;

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; :: thesis: ( 0 <= t9 & t9 <= 1 / 2 implies (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) )

assume ( 0 <= t9 & t9 <= 1 / 2 ) ; :: thesis: (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (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 TREAL_1:5 ;

hence (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) by A14, FUNCT_1:13; :: thesis: verum

end;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; :: thesis: ( 0 <= t9 & t9 <= 1 / 2 implies (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) )

assume ( 0 <= t9 & t9 <= 1 / 2 ) ; :: thesis: (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (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 TREAL_1:5 ;

hence (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) by A14, FUNCT_1:13; :: thesis: verum

.= 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;

A17: T2 is compact by HEINE:4;

dom g1 = the carrier of I[01] by FUNCT_2:def 1;

then A18: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) c= dom g1 by TOPMETR:20;

( dom g2 = 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 A19: dom (g2 * (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

then
not 0 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
by A8, A19, RCOMP_1:def 1;
assume
0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
; :: thesis: contradiction

then ex rr being Real st

( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ;

hence contradiction ; :: thesis: verum

end;then ex rr being Real st

( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ;

hence contradiction ; :: thesis: verum

then A20: ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 by FUNCT_4:11

.= g1 . (2 * 0) by A12

.= w1 by A2 ;

A21: dom ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) = (dom (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:def 1

.= [.0,(1 / 2).] \/ [.(1 / 2),1.] by A7, A8, A18, A19, RELAT_1:27

.= the carrier of I[01] by BORSUK_1:40, XXREAL_1:174 ;

rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= (rng (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:17;

then A22: rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= the carrier of G by XBOOLE_1:1;

A23: ( R^1 is T_2 & T1 is compact ) by HEINE:4, PCOMPS_1:34, TOPMETR:def 6;

reconsider f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) as Function of I[01],G by A21, A22, 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],G by A1, A4, A15, A16, A23, A17, COMPTS_1:20, TOPMETR:20;

1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;

then 1 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A8, A19, RCOMP_1:def 1;

then A24: f . 1 = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 by FUNCT_4:13

.= g2 . ((2 * 1) - 1) by A9

.= w3 by A6 ;

then w1,w3 are_connected by A20;

then reconsider f = f as Path of w1,w3 by A20, A24, Def2;

for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )

proof

hence
ex P0 being Path of w1,w3 st
let t be Point of I[01]; :: thesis: for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )

let t9 be Real; :: thesis: ( t = t9 implies ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ) )

assume A25: t = t9 ; :: thesis: ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )

thus ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) :: thesis: ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) )

end;( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )

let t9 be Real; :: thesis: ( t = t9 implies ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ) )

assume A25: t = t9 ; :: thesis: ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )

thus ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) :: thesis: ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) )

proof

thus
( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) )
:: thesis: verum
assume A26:
( 0 <= t9 & t9 <= 1 / 2 )
; :: thesis: f . t = g1 . (2 * t9)

then t9 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;

then A27: t9 in [.0,(1 / 2).] by RCOMP_1:def 1;

end;then t9 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;

then A27: t9 in [.0,(1 / 2).] by RCOMP_1:def 1;

per cases
( t9 <> 1 / 2 or t9 = 1 / 2 )
;

end;

suppose A28:
t9 <> 1 / 2
; :: thesis: f . t = g1 . (2 * t9)

not t9 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))

.= g1 . (2 * t9) by A12, A25, A26 ;

hence f . t = g1 . (2 * t9) ; :: thesis: verum

end;proof

then f . t =
(g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t
by A25, FUNCT_4:11
assume
t9 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
; :: thesis: contradiction

then t9 in [.0,(1 / 2).] /\ [.(1 / 2),1.] by A8, A19, A27, XBOOLE_0:def 4;

then t9 in {(1 / 2)} by XXREAL_1:418;

hence contradiction by A28, TARSKI:def 1; :: thesis: verum

end;then t9 in [.0,(1 / 2).] /\ [.(1 / 2),1.] by A8, A19, A27, XBOOLE_0:def 4;

then t9 in {(1 / 2)} by XXREAL_1:418;

hence contradiction by A28, TARSKI:def 1; :: thesis: verum

.= g1 . (2 * t9) by A12, A25, A26 ;

hence f . t = g1 . (2 * t9) ; :: thesis: verum

suppose A29:
t9 = 1 / 2
; :: thesis: f . t = g1 . (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 (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A25, A29, FUNCT_2:def 1, TOPMETR:20;

then f . t = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . (1 / 2) by A25, A29, FUNCT_4:13

.= g1 . (2 * t9) by A12, A15, A29 ;

hence f . t = g1 . (2 * t9) ; :: thesis: verum

end;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 (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A25, A29, FUNCT_2:def 1, TOPMETR:20;

then f . t = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . (1 / 2) by A25, A29, FUNCT_4:13

.= g1 . (2 * t9) by A12, A15, A29 ;

hence f . t = g1 . (2 * t9) ; :: thesis: verum

proof

assume A30:
( 1 / 2 <= t9 & t9 <= 1 )
; :: thesis: f . t = g2 . ((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 = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t by A8, A19, A25, FUNCT_4:13

.= g2 . ((2 * t9) - 1) by A9, A25, A30 ;

hence f . t = g2 . ((2 * t9) - 1) ; :: thesis: verum

end;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 = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t by A8, A19, A25, FUNCT_4:13

.= g2 . ((2 * t9) - 1) by A9, A25, A30 ;

hence f . t = g2 . ((2 * t9) - 1) ; :: thesis: verum

( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) ) by A20, A24; :: thesis: verum

A31: ( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 ) and

A32: for t being Point of I[01]

for t9 being Real st t = t9 holds

( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ;

rng P0 c= (rng g1) \/ (rng g2)

proof

hence
ex h3 being Function of I[01],G st
A33:
dom g2 = the carrier of I[01]
by FUNCT_2:def 1;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P0 or x in (rng g1) \/ (rng g2) )

A34: dom g1 = the carrier of I[01] by FUNCT_2:def 1;

assume x in rng P0 ; :: thesis: x in (rng g1) \/ (rng g2)

then consider z being object such that

A35: z in dom P0 and

A36: x = P0 . z by FUNCT_1:def 3;

reconsider r = z as Real by A35;

A37: 0 <= r by A35, BORSUK_1:40, XXREAL_1:1;

A38: r <= 1 by A35, BORSUK_1:40, XXREAL_1:1;

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P0 or x in (rng g1) \/ (rng g2) )

A34: dom g1 = the carrier of I[01] by FUNCT_2:def 1;

assume x in rng P0 ; :: thesis: x in (rng g1) \/ (rng g2)

then consider z being object such that

A35: z in dom P0 and

A36: x = P0 . z by FUNCT_1:def 3;

reconsider r = z as Real by A35;

A37: 0 <= r by A35, BORSUK_1:40, XXREAL_1:1;

A38: r <= 1 by A35, BORSUK_1:40, XXREAL_1:1;

per cases
( r <= 1 / 2 or r > 1 / 2 )
;

end;

suppose A39:
r <= 1 / 2
; :: thesis: x in (rng g1) \/ (rng g2)

then A40:
2 * r <= 2 * (1 / 2)
by XREAL_1:64;

0 <= 2 * r by A37, XREAL_1:127;

then A41: 2 * r in the carrier of I[01] by A40, BORSUK_1:40, XXREAL_1:1;

P0 . z = g1 . (2 * r) by A32, A35, A37, A39;

then P0 . z in rng g1 by A34, A41, FUNCT_1:def 3;

hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def 3; :: thesis: verum

end;0 <= 2 * r by A37, XREAL_1:127;

then A41: 2 * r in the carrier of I[01] by A40, BORSUK_1:40, XXREAL_1:1;

P0 . z = g1 . (2 * r) by A32, A35, A37, A39;

then P0 . z in rng g1 by A34, A41, FUNCT_1:def 3;

hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def 3; :: thesis: verum

suppose A42:
r > 1 / 2
; :: thesis: x in (rng g1) \/ (rng g2)

2 * r <= 2 * 1
by A38, XREAL_1:64;

then 2 * r <= 1 + 1 ;

then A43: (2 * r) - 1 <= 1 by XREAL_1:20;

2 * (1 / 2) = 1 ;

then 0 + 1 <= 2 * r by A42, XREAL_1:64;

then 0 <= (2 * r) - 1 by XREAL_1:19;

then A44: (2 * r) - 1 in the carrier of I[01] by A43, BORSUK_1:40, XXREAL_1:1;

P0 . z = g2 . ((2 * r) - 1) by A32, A35, A38, A42;

then P0 . z in rng g2 by A33, A44, FUNCT_1:def 3;

hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def 3; :: thesis: verum

end;then 2 * r <= 1 + 1 ;

then A43: (2 * r) - 1 <= 1 by XREAL_1:20;

2 * (1 / 2) = 1 ;

then 0 + 1 <= 2 * r by A42, XREAL_1:64;

then 0 <= (2 * r) - 1 by XREAL_1:19;

then A44: (2 * r) - 1 in the carrier of I[01] by A43, BORSUK_1:40, XXREAL_1:1;

P0 . z = g2 . ((2 * r) - 1) by A32, A35, A38, A42;

then P0 . z in rng g2 by A33, A44, FUNCT_1:def 3;

hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def 3; :: thesis: verum

( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) by A31; :: thesis: verum