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