let T be non empty TopSpace; :: thesis:
let c1, c2 be with_endpoints Curve of T; :: thesis:
let S be Subset of R^1; :: thesis:
assume A1: ( dom c1 = dom c2 & S = dom c1 ) ; :: thesis:
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 ) ) ) ) :: thesis:

assume A8: c1,c2 are_homotopic ; :: thesis:

suppose A9: inf (dom c1) < sup (dom c1) ; :: thesis:

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 ; :: thesis:
take a ; :: thesis:
take b ; :: thesis:
thus h is continuous by A11; :: thesis:
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 ) :: thesis:

proof

let t be Point of (R^1 | S); :: thesis:
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 ; :: thesis:
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 ; :: thesis:

end;

thus for t being Point of I[01] holds
( h . ((inf S),t) = a & h . ((sup S),t) = b ) :: thesis:

proof

let t be Point of I[01]; :: thesis:
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 ; :: thesis:
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 ; :: thesis:

end;

suppose not inf (dom c1) < sup (dom c1) ; :: thesis:

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); :: thesis:
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 ; :: thesis:
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 ; :: thesis:

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]; :: thesis:
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 ; :: thesis:
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 ; :: thesis:

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

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 ) ) ) ; :: thesis:
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]; :: thesis:
[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 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:

end;

then p1,p2 are_homotopic by A48;
hence c1,c2 are_homotopic ; :: thesis: