set e1 = P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) );
set e2 = P[01] (1 / 2),1,((#) 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: ( dom P = the carrier of I[01] & dom Q = the carrier of I[01] ) by FUNCT_2:def 1;
then A6: rng (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) c= dom P by TOPMETR:27;
rng (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) c= the carrier of (Closed-Interval-TSpace 0 ,1) ;
then A7: dom (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) = dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) by A5, RELAT_1:46, TOPMETR:27;
A8: 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, A6, A7, RELAT_1:46
.= the carrier of I[01] by BORSUK_1:83, XXREAL_1:174 ;
A9: for t' being Real st 0 <= t' & t' <= 1 / 2 holds
(P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = P . (2 * t')

proof

let t' be Real; :: thesis:
assume A10: ( 0 <= t' & t' <= 1 / 2 ) ; :: thesis:
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 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 ;
then A11: t' in dom (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) by A10;
then reconsider s = t' as Point of (Closed-Interval-TSpace 0 ,(1 / 2)) ;
reconsider r1 = (#) 0 ,1, r2 = 0 ,1 (#) as Real by TREAL_1:8;
(P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) . s = (((r2 - r1) / ((1 / 2) - 0 )) * t') + ((((1 / 2) * r1) - (0 * r2)) / (1 / 2)) by TREAL_1:14
.= 2 * t' by TREAL_1:8 ;
hence (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t' = P . (2 * t') by A11, FUNCT_1:23; :: thesis:

end;

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:
then ex rr being Real st
( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ;
hence contradiction ; :: thesis:

end;

then not 0 in dom (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) by A4, A7, RCOMP_1:def 1;
then A12: ((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 A9
.= a by A1, Def2 ;
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 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;
then 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 A8, FUNCT_2:def 1, RELSET_1:11;
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;
A13: P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ) is continuous Function of (Closed-Interval-TSpace 0 ,(1 / 2)),(Closed-Interval-TSpace 0 ,1) by TREAL_1:15;
A14: P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ) is continuous by TREAL_1:15;
reconsider ff = P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) )) as Function of T1,T by TOPMETR:27;
A15: Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) is Function of the carrier of (Closed-Interval-TSpace (1 / 2),1),the carrier of T by TOPMETR:27;
reconsider gg = Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) as Function of T2,T by TOPMETR:27;
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;
( P is continuous & Q is continuous ) by A1, A2, Def2;
then A16: ( ff is continuous & gg is continuous ) by A13, A14, TOPMETR:27;
A17: [#] T1 = [.0 ,(1 / 2).] by TOPMETR:25;
A18: [#] T2 = [.(1 / 2),1.] by TOPMETR:25;
then A19: ([#] T1) \/ ([#] T2) = [#] I[01] by A17, BORSUK_1:83, XXREAL_1:174;
A20: for t' being Real st 1 / 2 <= t' & t' <= 1 holds
(Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = Q . ((2 * t') - 1)

proof

let t' be Real; :: thesis:
assume A21: ( 1 / 2 <= t' & t' <= 1 ) ; :: thesis:
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 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 ;
then A22: t' in dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) by A21;
then reconsider s = t' as Point of (Closed-Interval-TSpace (1 / 2),1) ;
reconsider r1 = (#) 0 ,1, r2 = 0 ,1 (#) as Real by TREAL_1:8;
(P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) . s = (((r2 - r1) / (1 - (1 / 2))) * t') + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by TREAL_1:14
.= (2 * t') - 1 by TREAL_1:8 ;
hence (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . t' = Q . ((2 * t') - 1) by A22, FUNCT_1:23; :: thesis:

end;

A23: ff . (1 / 2) = P . (2 * (1 / 2)) by A9
.= b by A1, Def2
.= Q . ((2 * (1 / 2)) - 1) by A2, Def2
.= gg . pol by A20 ;
A24: ([#] T1) /\ ([#] T2) = {pol} by A17, A18, XXREAL_1:418;
R^1 is T_2 by PCOMPS_1:38, TOPMETR:def 7;
then ( T1 is compact & T2 is compact & I[01] is T_2 & ff . pol = gg . pol ) by A23, HEINE:11;
then reconsider f = f as continuous Function of I[01] ,T by A16, A19, A24, COMPTS_1:29;
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, A7, RCOMP_1:def 1;
then A25: f . 1 = (Q * (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))) . 1 by FUNCT_4:14
.= Q . ((2 * 1) - 1) by A20
.= c by A2, Def2 ;
then a,c are_connected by A12, Def1;
then reconsider f = f as Path of a,c by A12, A25, 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:
A26: ( 0 <= t & t <= 1 ) by Lm1;
A27: t is Real by XREAL_0:def 1;
thus ( t <= 1 / 2 implies f . t = P . (2 * t) ) :: thesis:

proof

assume A28: t <= 1 / 2 ; :: thesis:
then t in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by A26, A27;
then A29: t in [.0 ,(1 / 2).] by RCOMP_1:def 1;

per cases ;

suppose A30: t <> 1 / 2 ; :: thesis:

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:
then t in [.0 ,(1 / 2).] /\ [.(1 / 2),1.] by A4, A7, A29, XBOOLE_0:def 4;
then t in {(1 / 2)} by XXREAL_1:418;
hence contradiction by A30, TARSKI:def 1; :: thesis:

end;

then f . t = (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t by FUNCT_4:12
.= P . (2 * t) by A9, A26, A27, A28 ;
hence f . t = P . (2 * t) ; :: thesis:

end;

suppose A31: t = 1 / 2 ; :: thesis:

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 A15, A31, FUNCT_2:def 1;
then f . t = (P * (P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ))) . t by A23, A31, FUNCT_4:14
.= P . (2 * t) by A9, A26, A27, A28 ;
hence f . t = P . (2 * t) ; :: thesis:

end;

thus ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) :: thesis:

proof

assume A32: 1 / 2 <= t ; :: thesis:
then t in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by A26, A27;
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, A7, FUNCT_4:14
.= Q . ((2 * t) - 1) by A20, A26, A27, A32 ;
hence f . t = Q . ((2 * t) - 1) ; :: thesis:

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: