let T be non empty TopSpace; for c1, c2 being with_endpoints Curve of T
for S being Subset of R^1 st dom c1 = dom c2 & S = dom c1 holds
( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )
let c1, c2 be with_endpoints Curve of T; for S being Subset of R^1 st dom c1 = dom c2 & S = dom c1 holds
( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )
let S be Subset of R^1; ( dom c1 = dom c2 & S = dom c1 implies ( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) ) )
assume A1:
( dom c1 = dom c2 & S = dom c1 )
; ( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )
A2:
inf (dom c1) <= sup (dom c1)
by XXREAL_2:40;
A3:
S = [.(inf (dom c1)),(sup (dom c1)).]
by A1, Th27;
A4:
0 in [#] I[01]
by BORSUK_1:40, XXREAL_1:1;
A5:
1 in [#] I[01]
by BORSUK_1:40, XXREAL_1:1;
A6:
inf S in S
by A3, A2, A1, XXREAL_1:1;
A7:
sup S in S
by A3, A2, A1, XXREAL_1:1;
thus
( c1,c2 are_homotopic implies ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )
( ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) implies c1,c2 are_homotopic )proof
assume A8:
c1,
c2 are_homotopic
;
ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) )
per cases
( inf (dom c1) < sup (dom c1) or not inf (dom c1) < sup (dom c1) )
;
suppose A9:
inf (dom c1) < sup (dom c1)
;
ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) )consider a,
b being
Point of
T,
p1,
p2 being
Path of
a,
b such that A10:
(
p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) &
p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) &
p1,
p2 are_homotopic )
by A8;
consider f being
Function of
[:I[01],I[01]:],
T such that A11:
(
f is
continuous & ( for
t being
Point of
I[01] holds
(
f . (
t,
0)
= p1 . t &
f . (
t,1)
= p2 . t &
f . (
0,
t)
= a &
f . (1,
t)
= b ) ) )
by A10;
set f1 =
L[01] (
(inf (dom c1)),
(sup (dom c1)),
0,1);
set f2 =
L[01] (
0,1,
0,1);
reconsider S1 =
R^1 | S as non
empty TopSpace by A1;
A12:
Closed-Interval-TSpace (
(inf (dom c1)),
(sup (dom c1)))
= S1
by A3, A9, TOPMETR:19;
reconsider f1 =
L[01] (
(inf (dom c1)),
(sup (dom c1)),
0,1) as
continuous Function of
S1,
I[01] by A9, A12, BORSUK_6:34, TOPMETR:20;
reconsider f2 =
L[01] (
0,1,
0,1) as
continuous Function of
I[01],
I[01] by BORSUK_6:34, TOPMETR:20;
set h =
f * [:f1,f2:];
reconsider h =
f * [:f1,f2:] as
Function of
[:(R^1 | S),I[01]:],
T ;
take
h
;
ex a, b being Point of T st
( h is continuous & ( for t being Point of (R^1 | S) holds
( h . (t,0) = c1 . t & h . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( h . ((inf S),t) = a & h . ((sup S),t) = b ) ) )take
a
;
ex b being Point of T st
( h is continuous & ( for t being Point of (R^1 | S) holds
( h . (t,0) = c1 . t & h . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( h . ((inf S),t) = a & h . ((sup S),t) = b ) ) )take
b
;
( h is continuous & ( for t being Point of (R^1 | S) holds
( h . (t,0) = c1 . t & h . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( h . ((inf S),t) = a & h . ((sup S),t) = b ) ) )thus
h is
continuous
by A11;
( ( for t being Point of (R^1 | S) holds
( h . (t,0) = c1 . t & h . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( h . ((inf S),t) = a & h . ((sup S),t) = b ) ) )A13:
dom f1 = [#] (R^1 | S)
by FUNCT_2:def 1;
A14:
dom f2 = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
A15:
f2 . 0 =
(((1 - 0) / (1 - 0)) * (0 - 0)) + 0
by BORSUK_6:35
.=
0
;
A16:
f2 . 1 =
(((1 - 0) / (1 - 0)) * (1 - 0)) + 0
by BORSUK_6:35
.=
1
;
A17:
rng f1 c= [#] I[01]
by RELAT_1:def 19;
A18:
0 in dom f2
by A14, XXREAL_1:1;
A19:
1
in dom f2
by A14, XXREAL_1:1;
A20:
(sup (dom c1)) - (inf (dom c1)) <> 0
by A9;
thus
for
t being
Point of
(R^1 | S) holds
(
h . (
t,
0)
= c1 . t &
h . (
t,1)
= c2 . t )
for t being Point of I[01] holds
( h . ((inf S),t) = a & h . ((sup S),t) = b )proof
let t be
Point of
(R^1 | S);
( h . (t,0) = c1 . t & h . (t,1) = c2 . t )
A21:
t in dom f1
by A13;
[t,0] in [:(dom f1),(dom f2):]
by A13, A18, ZFMISC_1:def 2;
then A22:
[t,0] in dom [:f1,f2:]
by FUNCT_3:def 8;
[t,1] in [:(dom f1),(dom f2):]
by A13, A19, ZFMISC_1:def 2;
then A23:
[t,1] in dom [:f1,f2:]
by FUNCT_3:def 8;
A24:
f1 . t in rng f1
by A13, FUNCT_1:3;
A25:
t in S
by A21, A13, PRE_TOPC:def 5;
t in [#] (Closed-Interval-TSpace ((inf (dom c1)),(sup (dom c1))))
by A12;
then A26:
t in dom (L[01] ((inf (dom c1)),(sup (dom c1)),(inf (dom c1)),(sup (dom c1))))
by FUNCT_2:def 1;
A27:
(
inf (dom c1) <= t &
t <= sup (dom c1) )
by A25, A3, XXREAL_1:1;
A28:
(L[01] ((inf (dom c1)),(sup (dom c1)),(inf (dom c1)),(sup (dom c1)))) . t =
((((sup (dom c1)) - (inf (dom c1))) / ((sup (dom c1)) - (inf (dom c1)))) * (t - (inf (dom c1)))) + (inf (dom c1))
by A27, A9, BORSUK_6:35
.=
(1 * (t - (inf (dom c1)))) + (inf (dom c1))
by A20, XCMPLX_1:60
.=
t
;
thus h . (
t,
0) =
h . [t,0]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [t,0])
by A22, FUNCT_1:13
.=
f . ([:f1,f2:] . (t,0))
by BINOP_1:def 1
.=
f . [(f1 . t),(f2 . 0)]
by A13, A18, FUNCT_3:def 8
.=
f . (
(f1 . t),
0)
by A15, BINOP_1:def 1
.=
p1 . (f1 . t)
by A24, A11, A17
.=
((c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1))))) * f1) . t
by A10, A13, FUNCT_1:13
.=
(c1 * ((L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) * f1)) . t
by RELAT_1:36
.=
(c1 * (L[01] ((inf (dom c1)),(sup (dom c1)),(inf (dom c1)),(sup (dom c1))))) . t
by Th2, A9
.=
c1 . t
by A28, A26, FUNCT_1:13
;
h . (t,1) = c2 . t
thus h . (
t,1) =
h . [t,1]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [t,1])
by A23, FUNCT_1:13
.=
f . ([:f1,f2:] . (t,1))
by BINOP_1:def 1
.=
f . [(f1 . t),(f2 . 1)]
by A13, A19, FUNCT_3:def 8
.=
f . (
(f1 . t),1)
by A16, BINOP_1:def 1
.=
p2 . (f1 . t)
by A24, A11, A17
.=
((c2 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1))))) * f1) . t
by A10, A1, A13, FUNCT_1:13
.=
(c2 * ((L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) * f1)) . t
by RELAT_1:36
.=
(c2 * (L[01] ((inf (dom c1)),(sup (dom c1)),(inf (dom c1)),(sup (dom c1))))) . t
by Th2, A9
.=
c2 . t
by A28, A26, FUNCT_1:13
;
verum
end; thus
for
t being
Point of
I[01] holds
(
h . (
(inf S),
t)
= a &
h . (
(sup S),
t)
= b )
verumproof
let t be
Point of
I[01];
( h . ((inf S),t) = a & h . ((sup S),t) = b )
A29:
inf S in dom f1
by A6, A13, PRE_TOPC:def 5;
A30:
sup S in dom f1
by A7, A13, PRE_TOPC:def 5;
t in [#] I[01]
;
then A31:
t in dom f2
by FUNCT_2:def 1;
[(inf S),t] in [:(dom f1),(dom f2):]
by A31, A29, ZFMISC_1:def 2;
then A32:
[(inf S),t] in dom [:f1,f2:]
by FUNCT_3:def 8;
[(sup S),t] in [:(dom f1),(dom f2):]
by A31, A30, ZFMISC_1:def 2;
then A33:
[(sup S),t] in dom [:f1,f2:]
by FUNCT_3:def 8;
(
0 <= t &
t <= 1 )
by BORSUK_1:40, XXREAL_1:1;
then A34:
f2 . t =
(((1 - 0) / (1 - 0)) * (t - 0)) + 0
by BORSUK_6:35
.=
t
;
A35:
f1 . (inf S) =
(((1 - 0) / ((sup (dom c1)) - (inf (dom c1)))) * ((inf (dom c1)) - (inf (dom c1)))) + 0
by A1, A9, BORSUK_6:35
.=
0
;
A36:
f1 . (sup S) =
(((1 - 0) / ((sup (dom c1)) - (inf (dom c1)))) * ((sup (dom c1)) - (inf (dom c1)))) + 0
by A1, A9, BORSUK_6:35
.=
(((sup (dom c1)) - (inf (dom c1))) / ((sup (dom c1)) - (inf (dom c1)))) * 1
by XCMPLX_1:75
.=
1
by A20, XCMPLX_1:60
;
thus h . (
(inf S),
t) =
h . [(inf S),t]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [(inf S),t])
by A32, FUNCT_1:13
.=
f . ([:f1,f2:] . ((inf S),t))
by BINOP_1:def 1
.=
f . [(f1 . (inf S)),(f2 . t)]
by A31, A29, FUNCT_3:def 8
.=
f . (
(f1 . (inf S)),
t)
by A34, BINOP_1:def 1
.=
a
by A11, A35
;
h . ((sup S),t) = b
thus h . (
(sup S),
t) =
h . [(sup S),t]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [(sup S),t])
by A33, FUNCT_1:13
.=
f . ([:f1,f2:] . ((sup S),t))
by BINOP_1:def 1
.=
f . [(f1 . (sup S)),(f2 . t)]
by A31, A30, FUNCT_3:def 8
.=
f . (
(f1 . (sup S)),
t)
by A34, BINOP_1:def 1
.=
b
by A11, A36
;
verum
end; end; suppose
not
inf (dom c1) < sup (dom c1)
;
ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) )then
inf (dom c1) = sup (dom c1)
by A2, XXREAL_0:1;
then
dom c1 = [.(inf (dom c1)),(inf (dom c1)).]
by Th27;
then A37:
dom c1 = {(inf (dom c1))}
by XXREAL_1:17;
set a =
the_first_point_of c1;
set f =
[:(R^1 | S),I[01]:] --> (the_first_point_of c1);
A38:
for
t being
Point of
(R^1 | S) holds
(
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
t,
0)
= c1 . t &
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
t,1)
= c2 . t )
proof
let t be
Point of
(R^1 | S);
( ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (t,0) = c1 . t & ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (t,1) = c2 . t )
A39:
t in [#] (R^1 | S)
by A1, SUBSET_1:def 1;
A40:
[t,0] in [:([#] (R^1 | S)),([#] I[01]):]
by A4, A1, ZFMISC_1:def 2;
A41:
[t,1] in [:([#] (R^1 | S)),([#] I[01]):]
by A5, A1, ZFMISC_1:def 2;
A42:
t in S
by A39, PRE_TOPC:def 5;
then A43:
t = inf (dom c1)
by A1, A37, TARSKI:def 1;
thus ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
t,
0) =
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . [t,0]
by BINOP_1:def 1
.=
c1 . t
by A43, A40, FUNCOP_1:7
;
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (t,1) = c2 . t
thus ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
t,1) =
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . [t,1]
by BINOP_1:def 1
.=
the_first_point_of c1
by A41, FUNCOP_1:7
.=
the_first_point_of c2
by A8, Th35
.=
c2 . t
by A1, A42, A37, TARSKI:def 1
;
verum
end;
for
t being
Point of
I[01] holds
(
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
(inf S),
t)
= the_first_point_of c1 &
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
(sup S),
t)
= the_first_point_of c1 )
proof
let t be
Point of
I[01];
( ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . ((inf S),t) = the_first_point_of c1 & ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . ((sup S),t) = the_first_point_of c1 )
A44:
inf S in [#] (R^1 | S)
by A6, PRE_TOPC:def 5;
A45:
sup S in [#] (R^1 | S)
by A7, PRE_TOPC:def 5;
A46:
[(inf S),t] in [:([#] (R^1 | S)),([#] I[01]):]
by A44, ZFMISC_1:def 2;
A47:
[(sup S),t] in [:([#] (R^1 | S)),([#] I[01]):]
by A45, ZFMISC_1:def 2;
thus ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
(inf S),
t) =
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . [(inf S),t]
by BINOP_1:def 1
.=
the_first_point_of c1
by A46, FUNCOP_1:7
;
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . ((sup S),t) = the_first_point_of c1
thus ([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . (
(sup S),
t) =
([:(R^1 | S),I[01]:] --> (the_first_point_of c1)) . [(sup S),t]
by BINOP_1:def 1
.=
the_first_point_of c1
by A47, FUNCOP_1:7
;
verum
end; hence
ex
f being
Function of
[:(R^1 | S),I[01]:],
T ex
a,
b being
Point of
T st
(
f is
continuous & ( for
t being
Point of
(R^1 | S) holds
(
f . (
t,
0)
= c1 . t &
f . (
t,1)
= c2 . t ) ) & ( for
t being
Point of
I[01] holds
(
f . (
(inf S),
t)
= a &
f . (
(sup S),
t)
= b ) ) )
by A38;
verum end; end;
end;
given f being Function of [:(R^1 | S),I[01]:],T, a, b being Point of T such that A48:
( f is continuous & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) )
; c1,c2 are_homotopic
A49:
inf S in [#] (R^1 | S)
by A6, PRE_TOPC:def 5;
A50:
sup S in [#] (R^1 | S)
by A7, PRE_TOPC:def 5;
A51: a =
f . ((inf S),0)
by A4, A48
.=
the_first_point_of c1
by A1, A49, A48
;
b =
f . ((sup S),0)
by A4, A48
.=
the_last_point_of c1
by A1, A50, A48
;
then reconsider p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) as Path of a,b by A51, Th29;
A52: a =
f . ((inf S),1)
by A5, A48
.=
the_first_point_of c2
by A1, A49, A48
;
b =
f . ((sup S),1)
by A5, A48
.=
the_last_point_of c2
by A1, A50, A48
;
then reconsider p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) as Path of a,b by A52, Th29;
set f1 = L[01] (0,1,(inf (dom c1)),(sup (dom c1)));
set f2 = L[01] (0,1,0,1);
reconsider S1 = R^1 | S as non empty TopSpace by A1;
A53:
Closed-Interval-TSpace ((inf (dom c1)),(sup (dom c1))) = S1
by A3, A2, TOPMETR:19;
reconsider f1 = L[01] (0,1,(inf (dom c1)),(sup (dom c1))) as continuous Function of I[01],S1 by A2, A53, BORSUK_6:34, TOPMETR:20;
reconsider f2 = L[01] (0,1,0,1) as continuous Function of I[01],I[01] by BORSUK_6:34, TOPMETR:20;
set h = f * [:f1,f2:];
reconsider h = f * [:f1,f2:] as Function of [:I[01],I[01]:],T ;
A54:
dom f1 = [#] I[01]
by FUNCT_2:def 1;
A55:
dom f2 = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
A56: f2 . 0 =
(((1 - 0) / (1 - 0)) * (0 - 0)) + 0
by BORSUK_6:35
.=
0
;
A57: f2 . 1 =
(((1 - 0) / (1 - 0)) * (1 - 0)) + 0
by BORSUK_6:35
.=
1
;
A58:
0 in dom f2
by A55, XXREAL_1:1;
A59:
1 in dom f2
by A55, XXREAL_1:1;
for t being Point of I[01] holds
( h . (t,0) = p1 . t & h . (t,1) = p2 . t & h . (0,t) = a & h . (1,t) = b )
proof
let t be
Point of
I[01];
( h . (t,0) = p1 . t & h . (t,1) = p2 . t & h . (0,t) = a & h . (1,t) = b )
[t,0] in [:(dom f1),(dom f2):]
by A54, A58, ZFMISC_1:def 2;
then A60:
[t,0] in dom [:f1,f2:]
by FUNCT_3:def 8;
[t,1] in [:(dom f1),(dom f2):]
by A54, A59, ZFMISC_1:def 2;
then A61:
[t,1] in dom [:f1,f2:]
by FUNCT_3:def 8;
A62:
0 in dom f1
by A54, BORSUK_1:40, XXREAL_1:1;
A63:
1
in dom f1
by A54, BORSUK_1:40, XXREAL_1:1;
[0,t] in [:(dom f1),(dom f2):]
by A62, A55, BORSUK_1:40, ZFMISC_1:def 2;
then A64:
[0,t] in dom [:f1,f2:]
by FUNCT_3:def 8;
[1,t] in [:(dom f1),(dom f2):]
by A63, A55, BORSUK_1:40, ZFMISC_1:def 2;
then A65:
[1,t] in dom [:f1,f2:]
by FUNCT_3:def 8;
A66:
f1 . 0 =
((((sup (dom c1)) - (inf (dom c1))) / (1 - 0)) * (0 - 0)) + (inf (dom c1))
by A2, BORSUK_6:35
.=
inf S
by A1
;
A67:
f1 . 1 =
((((sup (dom c1)) - (inf (dom c1))) / (1 - 0)) * (1 - 0)) + (inf (dom c1))
by A2, BORSUK_6:35
.=
sup S
by A1
;
(
0 <= t &
t <= 1 )
by BORSUK_1:40, XXREAL_1:1;
then A68:
f2 . t =
(((1 - 0) / (1 - 0)) * (t - 0)) + 0
by BORSUK_6:35
.=
t
;
thus h . (
t,
0) =
h . [t,0]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [t,0])
by A60, FUNCT_1:13
.=
f . ([:f1,f2:] . (t,0))
by BINOP_1:def 1
.=
f . [(f1 . t),(f2 . 0)]
by A54, A58, FUNCT_3:def 8
.=
f . (
(f1 . t),
0)
by A56, BINOP_1:def 1
.=
c1 . (f1 . t)
by A48
.=
p1 . t
by A54, FUNCT_1:13
;
( h . (t,1) = p2 . t & h . (0,t) = a & h . (1,t) = b )
thus h . (
t,1) =
h . [t,1]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [t,1])
by A61, FUNCT_1:13
.=
f . ([:f1,f2:] . (t,1))
by BINOP_1:def 1
.=
f . [(f1 . t),(f2 . 1)]
by A54, A59, FUNCT_3:def 8
.=
f . (
(f1 . t),1)
by A57, BINOP_1:def 1
.=
c2 . (f1 . t)
by A48
.=
p2 . t
by A1, A54, FUNCT_1:13
;
( h . (0,t) = a & h . (1,t) = b )
thus h . (
0,
t) =
h . [0,t]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [0,t])
by A64, FUNCT_1:13
.=
f . ([:f1,f2:] . (0,t))
by BINOP_1:def 1
.=
f . [(f1 . 0),(f2 . t)]
by A62, A55, BORSUK_1:40, FUNCT_3:def 8
.=
f . (
(inf S),
t)
by A66, A68, BINOP_1:def 1
.=
a
by A48
;
h . (1,t) = b
thus h . (1,
t) =
h . [1,t]
by BINOP_1:def 1
.=
f . ([:f1,f2:] . [1,t])
by A65, FUNCT_1:13
.=
f . ([:f1,f2:] . (1,t))
by BINOP_1:def 1
.=
f . [(f1 . 1),(f2 . t)]
by A63, A55, BORSUK_1:40, FUNCT_3:def 8
.=
f . (
(sup S),
t)
by A67, A68, BINOP_1:def 1
.=
b
by A48
;
verum
end;
then
p1,p2 are_homotopic
by A48;
hence
c1,c2 are_homotopic
; verum