let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T holds c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c

let c be with_endpoints Curve of T; :: thesis: c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c

set t1 = the_first_point_of c;

set t2 = the_last_point_of c;

reconsider c0 = c as parametrized-curve PartFunc of R^1,T by Th23;

consider S being SubSpace of R^1 , g being Function of S,T such that

A1: ( c0 = g & S = R^1 | (dom c0) & g is continuous ) by Def4;

reconsider S = S as non empty TopStruct by A1;

A2: inf (dom c) <= sup (dom c) by XXREAL_2:40;

then A3: L[01] (0,1,(inf (dom c)),(sup (dom c))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace ((inf (dom c)),(sup (dom c)))) by BORSUK_6:34;

A4: dom c0 = [.(inf (dom c)),(sup (dom c)).] by Th27;

then A5: Closed-Interval-TSpace ((inf (dom c)),(sup (dom c))) = S by A2, A1, TOPMETR:19;

reconsider f = L[01] (0,1,(inf (dom c)),(sup (dom c))) as Function of I[01],S by A4, A2, A1, TOPMETR:19, TOPMETR:20;

reconsider p = g * f as Function of I[01],T ;

A6: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;

A7: dom (L[01] (0,1,(inf (dom c)),(sup (dom c)))) = the carrier of (Closed-Interval-TSpace (0,1)) by FUNCT_2:def 1

.= [.0,1.] by TOPMETR:18 ;

A8: (L[01] (0,1,(inf (dom c)),(sup (dom c)))) . 0 = ((((sup (dom c)) - (inf (dom c))) / (1 - 0)) * (0 - 0)) + (inf (dom c)) by A2, BORSUK_6:35

.= inf (dom c) ;

A9: (L[01] (0,1,(inf (dom c)),(sup (dom c)))) . 1 = ((((sup (dom c)) - (inf (dom c))) / (1 - 0)) * (1 - 0)) + (inf (dom c)) by A2, BORSUK_6:35

.= sup (dom c) ;

A10: p is continuous by A1, A3, A5, TOPMETR:20, TOPS_2:46;

A11: p . 0 = the_first_point_of c by A8, A1, A6, A7, FUNCT_1:13;

A12: p . 1 = the_last_point_of c by A9, A1, A6, A7, FUNCT_1:13;

then the_first_point_of c, the_last_point_of c are_connected by A10, A11;

hence c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c by A1, A10, A11, A12, BORSUK_2:def 2; :: thesis: verum

let c be with_endpoints Curve of T; :: thesis: c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c

set t1 = the_first_point_of c;

set t2 = the_last_point_of c;

reconsider c0 = c as parametrized-curve PartFunc of R^1,T by Th23;

consider S being SubSpace of R^1 , g being Function of S,T such that

A1: ( c0 = g & S = R^1 | (dom c0) & g is continuous ) by Def4;

reconsider S = S as non empty TopStruct by A1;

A2: inf (dom c) <= sup (dom c) by XXREAL_2:40;

then A3: L[01] (0,1,(inf (dom c)),(sup (dom c))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace ((inf (dom c)),(sup (dom c)))) by BORSUK_6:34;

A4: dom c0 = [.(inf (dom c)),(sup (dom c)).] by Th27;

then A5: Closed-Interval-TSpace ((inf (dom c)),(sup (dom c))) = S by A2, A1, TOPMETR:19;

reconsider f = L[01] (0,1,(inf (dom c)),(sup (dom c))) as Function of I[01],S by A4, A2, A1, TOPMETR:19, TOPMETR:20;

reconsider p = g * f as Function of I[01],T ;

A6: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;

A7: dom (L[01] (0,1,(inf (dom c)),(sup (dom c)))) = the carrier of (Closed-Interval-TSpace (0,1)) by FUNCT_2:def 1

.= [.0,1.] by TOPMETR:18 ;

A8: (L[01] (0,1,(inf (dom c)),(sup (dom c)))) . 0 = ((((sup (dom c)) - (inf (dom c))) / (1 - 0)) * (0 - 0)) + (inf (dom c)) by A2, BORSUK_6:35

.= inf (dom c) ;

A9: (L[01] (0,1,(inf (dom c)),(sup (dom c)))) . 1 = ((((sup (dom c)) - (inf (dom c))) / (1 - 0)) * (1 - 0)) + (inf (dom c)) by A2, BORSUK_6:35

.= sup (dom c) ;

A10: p is continuous by A1, A3, A5, TOPMETR:20, TOPS_2:46;

A11: p . 0 = the_first_point_of c by A8, A1, A6, A7, FUNCT_1:13;

A12: p . 1 = the_last_point_of c by A9, A1, A6, A7, FUNCT_1:13;

then the_first_point_of c, the_last_point_of c are_connected by A10, A11;

hence c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c by A1, A10, A11, A12, BORSUK_2:def 2; :: thesis: verum