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:20, TREAL_1:8;
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:20;
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:20;
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:7
.= 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] ;
A9: dom [:fA,fB:] = [:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] by FUNCT_3:def 8;
A10: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by A3, Lm1;
then A11: [s,1] in dom [:fA,fB:] by A9, ZFMISC_1:87;
A12: 0 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by A3, Lm1;
then A13: [s,0] in dom [:fA,fB:] by A9, ZFMISC_1:87;
[:fA,fB:] . (s,1) = [((id the carrier of I[01]) . s),((L[01] (((0,1) (#)),((#) (0,1)))) . 1)] by A8, A10, FUNCT_3:def 8
.= [s,((L[01] (((0,1) (#)),((#) (0,1)))) . 1[01])]
.= [s,(1 - 1)] by A5
.= [s,0] ;
then A14: ff . (s,1) = f . (s,0) by A11, FUNCT_1:13
.= 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 8
.= [s,((L[01] (((0,1) (#)),((#) (0,1)))) . 0[01])]
.= [s,(1 - 0)] by A5
.= [s,1] ;
then ff . (s,0) = f . (s,1) by A13, FUNCT_1:13
.= 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 )
reconsider tt = t as Real ;
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:20;
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:7
.= 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:20;
A20: 0 in dom (id the carrier of I[01]) by Lm1;
A21: dom [:fA,fB:] = [:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] by FUNCT_3:def 8;
then A22: [0,t] in dom [:fA,fB:] by A19, A20, ZFMISC_1:87;
A23: 1 in dom (id the carrier of I[01]) by Lm1;
then A24: [1,t] in dom [:fA,fB:] by A19, A21, ZFMISC_1:87;
[:fA,fB:] . (1,t) = [((id the carrier of I[01]) . 1),((L[01] (((0,1) (#)),((#) (0,1)))) . t)] by A19, A23, FUNCT_3:def 8
.= [1,(1 - tt)] by A18, A23, FUNCT_1:18 ;
then A25: ff . (1,t) = f . (1,t9) by A24, FUNCT_1:13
.= b by A2 ;
[:fA,fB:] . (0,t) = [((id the carrier of I[01]) . 0),((L[01] (((0,1) (#)),((#) (0,1)))) . t)] by A19, A20, FUNCT_3:def 8
.= [0,(1 - tt)] by A18, A20, FUNCT_1:18 ;
then ff . (0,t) = f . (0,t9) by A22, FUNCT_1:13
.= a by A2 ;
hence ( ff . (0,t) = a & ff . (1,t) = b ) by A25; :: thesis: verum
end;
ff is continuous by A1, TOPS_2:46;
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