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 )

( ff . (0,t) = a & ff . (1,t) = b )

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

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

A15:
for t being Point of I[01] holds
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

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;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

A8:
dom (id the carrier of I[01]) = the carrier of I[01]
;
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;(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

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

( ff . (0,t) = a & ff . (1,t) = b )

proof

ff is continuous
by A1, TOPS_2:46;
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

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;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

then A18:
(L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - tt
;
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;(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

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

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