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; ( 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 )
; 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];
( 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];
for t9 being Real st t = t9 holds
(L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9let t9 be
Real;
( t = t9 implies (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 )
assume A6:
t = t9
;
(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
;
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;
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];
( 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];
for t9 being Real st t = t9 holds
(L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9let t9 be
Real;
( t = t9 implies (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 )
assume A16:
t = t9
;
(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
;
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;
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; verum