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 & ( 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 ) ) )
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] ;
reconsider fB = L[01] (0 ,1 (#) ),((#) 0 ,1) as continuous Function of I[01] ,I[01] by TOPMETR:27, TREAL_1:11;
set F = [:fA,fB:];
A2: [:fA,fB:] is continuous by Th12;
A3: dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) = the carrier of I[01] by FUNCT_2:def 1, TOPMETR:27;
set LL = L[01] (0 ,1 (#) ),((#) 0 ,1);
reconsider ff = f * [:fA,fB:] as Function of [:I[01] ,I[01] :],T ;
A4: ff is continuous by A1, A2, TOPS_2:58;
A5: 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 )
A6: for t being Point of I[01]
for t' being Real st t = t' holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t'

proof

let t be Point of I[01] ; :: thesis: for t' being Real st t = t' holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t'
let t' be Real; :: thesis: ( t = t' implies (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t' )
assume A7: t = t' ; :: thesis: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t'
reconsider ee = t as Point of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
A8: ( 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) * t') + 1 by A7, A8, TREAL_1:10
.= 1 - (1 * t') ;
hence (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t' ; :: thesis: verum

end;

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

end;

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 )
A15: t in the carrier of I[01] ;
A16: dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) = the carrier of I[01] by FUNCT_2:def 1, TOPMETR:27;
reconsider tt = t as Real by A15, BORSUK_1:83;
for t being Point of I[01]
for t' being Real st t = t' holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t'

proof

let t be Point of I[01] ; :: thesis: for t' being Real st t = t' holds
(L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t'
let t' be Real; :: thesis: ( t = t' implies (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t' )
assume A17: t = t' ; :: thesis: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t'
reconsider ee = t as Point of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
A18: ( 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) * t') + 1 by A17, A18, TREAL_1:10
.= 1 - (1 * t') ;
hence (L[01] (0 ,1 (#) ),((#) 0 ,1)) . t = 1 - t' ; :: thesis: verum

end;

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

end;

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, A5; :: thesis: verum