id the carrier of I[01] = id I[01] ;
then reconsider fA = id the carrier of I[01] as continuous Function of I[01] ,I[01] ;
set LL = L[01] (0 ,1 (#) ),((#) 0 ,1);
reconsider fB = L[01] (0 ,1 (#) ),((#) 0 ,1) as continuous Function of I[01] ,I[01] by TOPMETR:27, TREAL_1:11;
let P, Q be Path of a,b; :: thesis: ( ex f being Function of [:I[01] ,I[01] :],T st
( f is continuous & ( for t being Point of I[01] holds
( f . t,0 = P . t & f . t,1 = Q . t & f . 0 ,t = a & f . 1,t = b ) ) ) implies ex f being Function of [:I[01] ,I[01] :],T st
( f is continuous & ( for t being Point of I[01] holds
( f . t,0 = Q . t & f . t,1 = P . t & f . 0 ,t = a & f . 1,t = b ) ) ) )
given f being Function of [:I[01] ,I[01] :],T such that A1: f is continuous and
A2: for s being Point of I[01] holds
( f . s,0 = P . s & f . s,1 = Q . s & f . 0 ,s = a & f . 1,s = b ) ; :: thesis: ex f being Function of [:I[01] ,I[01] :],T st
( f is continuous & ( for t being Point of I[01] holds
( f . t,0 = Q . t & f . t,1 = P . t & f . 0 ,t = a & f . 1,t = b ) ) )
set F = [:fA,fB:];
reconsider ff = f * [:fA,fB:] as Function of [:I[01] ,I[01] :],T ;
A3: dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) = the carrier of I[01] by FUNCT_2:def 1, TOPMETR:27;
A4: for s being Point of I[01] holds
( ff . s,0 = Q . s & ff . s,1 = P . s )

proof

let s be Point of I[01] ; :: thesis: ( ff . s,0 = Q . s & ff . s,1 = P . s )
A5: for t being Point of I[01]
for t9 being Real st t = t9 holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9

proof

let t be Point of I[01] ; :: thesis: for t9 being Real st t = t9 holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9
let t9 be Real; :: thesis: ( t = t9 implies (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9 )
assume A6: t = t9 ; :: thesis: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9
reconsider ee = t as Point of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
A7: ( 0 ,1 (#) = 1 & (#) 0 ,1 = 0 ) by TREAL_1:def 1, TREAL_1:def 2;
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = (L[01] (0 ,1 (#) ),((#) 0 ,1)) . ee
.= ((0 - 1) * t9) + 1 by A6, A7, TREAL_1:10
.= 1 - (1 * t9) ;
hence (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9 ; :: thesis: verum

end;

A8: dom (id the carrier of I[01] ) = the carrier of I[01] by FUNCT_2:def 1;
A9: dom [:fA,fB:] = [:(dom (id the carrier of I[01] )),(dom (L[01] (0 ,1 (#) ),((#) 0 ,1))):] by FUNCT_3:def 9;
A10: 1 in dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by A3, Lm1;
then A11: [s,1] in dom [:fA,fB:] by A8, A9, ZFMISC_1:106;
A12: 0 in dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by A3, Lm1;
then A13: [s,0 ] in dom [:fA,fB:] by A8, A9, ZFMISC_1:106;
[:fA,fB:] . s,1 = [((id the carrier of I[01] ) . s),((L[01] (0 ,1 (#) ),((#) 0 ,1)) . 1)] by A8, A10, FUNCT_3:def 9
.= [s,((L[01] (0 ,1 (#) ),((#) 0 ,1)) . 1[01] )] by FUNCT_1:35
.= [s,(1 - 1)] by A5
.= [s,0 ] ;
then A14: ff . s,1 = f . s,0 by A11, FUNCT_1:23
.= P . s by A2 ;
[:fA,fB:] . s,0 = [((id the carrier of I[01] ) . s),((L[01] (0 ,1 (#) ),((#) 0 ,1)) . 0 )] by A8, A12, FUNCT_3:def 9
.= [s,((L[01] (0 ,1 (#) ),((#) 0 ,1)) . 0[01] )] by FUNCT_1:35
.= [s,(1 - 0 )] by A5
.= [s,1] ;
then ff . s,0 = f . s,1 by A13, FUNCT_1:23
.= Q . s by A2 ;
hence ( ff . s,0 = Q . s & ff . s,1 = P . s ) by A14; :: thesis: verum

end;

A15: for t being Point of I[01] holds
( ff . 0 ,t = a & ff . 1,t = b )

proof

let t be Point of I[01] ; :: thesis: ( ff . 0 ,t = a & ff . 1,t = b )
t in the carrier of I[01] ;
then reconsider tt = t as Real by BORSUK_1:83;
for t being Point of I[01]
for t9 being Real st t = t9 holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9

proof

let t be Point of I[01] ; :: thesis: for t9 being Real st t = t9 holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9
let t9 be Real; :: thesis: ( t = t9 implies (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9 )
assume A16: t = t9 ; :: thesis: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9
reconsider ee = t as Point of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
A17: ( 0 ,1 (#) = 1 & (#) 0 ,1 = 0 ) by TREAL_1:def 1, TREAL_1:def 2;
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = (L[01] (0 ,1 (#) ),((#) 0 ,1)) . ee
.= ((0 - 1) * t9) + 1 by A16, A17, TREAL_1:10
.= 1 - (1 * t9) ;
hence (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t9 ; :: thesis: verum

end;

then A18: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - tt ;
reconsider t9 = 1 - tt as Point of I[01] by Lm5;
A19: dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) = the carrier of I[01] by FUNCT_2:def 1, TOPMETR:27;
A20: dom (id the carrier of I[01] ) = the carrier of I[01] by FUNCT_2:def 1;
then A21: 0 in dom (id the carrier of I[01] ) by Lm1;
A22: dom [:fA,fB:] = [:(dom (id the carrier of I[01] )),(dom (L[01] (0 ,1 (#) ),((#) 0 ,1))):] by FUNCT_3:def 9;
then A23: [0 ,t] in dom [:fA,fB:] by A19, A21, ZFMISC_1:106;
A24: 1 in dom (id the carrier of I[01] ) by A20, Lm1;
then A25: [1,t] in dom [:fA,fB:] by A19, A22, ZFMISC_1:106;
[:fA,fB:] . 1,t = [((id the carrier of I[01] ) . 1),((L[01] (0 ,1 (#) ),((#) 0 ,1)) . t)] by A19, A24, FUNCT_3:def 9
.= [1,(1 - tt)] by A18, A24, FUNCT_1:35 ;
then A26: ff . 1,t = f . 1,t9 by A25, FUNCT_1:23
.= b by A2 ;
[:fA,fB:] . 0 ,t = [((id the carrier of I[01] ) . 0 ),((L[01] (0 ,1 (#) ),((#) 0 ,1)) . t)] by A19, A21, FUNCT_3:def 9
.= [0 ,(1 - tt)] by A18, A21, FUNCT_1:35 ;
then ff . 0 ,t = f . 0 ,t9 by A23, FUNCT_1:23
.= a by A2 ;
hence ( ff . 0 ,t = a & ff . 1,t = b ) by A26; :: thesis: verum

end;

[:fA,fB:] is continuous by Th12;
then ff is continuous by A1, TOPS_2:58;
hence ex f being Function of [:I[01] ,I[01] :],T st
( f is continuous & ( for t being Point of I[01] holds
( f . t,0 = Q . t & f . t,1 = P . t & f . 0 ,t = a & f . 1,t = b ) ) ) by A4, A15; :: thesis: verum