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 = 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:18 ;
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:18 ;
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: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 A6: 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 (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) )
assume ( 1 / 2 <= t9 & t9 <= 1 ) ; :: thesis: (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:11
.= (2 * t9) - 1 by TREAL_1:5 ;
hence (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) by A7, FUNCT_1:13; :: thesis: verum

end;

reconsider gg = Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of T2,T by TOPMETR:20;
reconsider ff = P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of T1,T by TOPMETR:20;
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:12;
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:17;
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:4, PCOMPS_1:34, TOPMETR:def 6;
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: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 A12: 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 (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) )
assume ( 0 <= t9 & t9 <= 1 / 2 ) ; :: thesis: (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:11
.= 2 * t9 by TREAL_1:5 ;
hence (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) by A13, FUNCT_1:13; :: thesis: 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:20;
( 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: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 ) } ; :: thesis: contradiction
then ex rr being Real st
( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ;
hence contradiction ; :: thesis: 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:11
.= 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:27
.= the carrier of I[01] by BORSUK_1:40, XXREAL_1:174 ;
( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:18;
then A19: ( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} ) by BORSUK_1:40, XXREAL_1:174, XXREAL_1:418;
A20: T2 is compact by HEINE:4;
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:4;
( 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:20, TOPMETR:20;
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:13
.= 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]; :: thesis: ( ( 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) ) :: thesis: ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) )

proof

assume A24: t <= 1 / 2 ; :: thesis: 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 ; :: thesis: 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) (#))))) ; :: thesis: 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; :: thesis: verum

end;

then f . t = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by FUNCT_4:11
.= P . (2 * t) by A11, A23, A22, A24 ;
hence f . t = P . (2 * t) ; :: thesis: verum

end;

suppose A27: t = 1 / 2 ; :: thesis: 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:18;
then t in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A27, FUNCT_2:def 1, TOPMETR:20;
then f . t = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by A14, A27, FUNCT_4:13
.= P . (2 * t) by A11, A23, A22, A24 ;
hence f . t = P . (2 * t) ; :: thesis: verum

end;

end;

end;

A28: t <= 1 by Lm1;
thus ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) :: thesis: verum

proof

assume A29: 1 / 2 <= t ; :: thesis: 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:13
.= Q . ((2 * t) - 1) by A5, A28, A22, A29 ;
hence f . t = Q . ((2 * t) - 1) ; :: thesis: verum

end;

end;

hence ex b₁ being Path of a,c st
for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₁ . t = P . (2 * t) ) & ( 1 / 2 <= t implies b₁ . t = Q . ((2 * t) - 1) ) ) ; :: thesis: verum