let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T holds c * (L (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 (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 (0,1,(inf (dom c)),(sup (dom c))) is continuous Function of (),(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 ;
reconsider f = L (0,1,(inf (dom c)),(sup (dom c))) as Function of I,S by ;
reconsider p = g * f as Function of I,T ;
A6: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
A7: dom (L (0,1,(inf (dom c)),(sup (dom c)))) = the carrier of () by FUNCT_2:def 1
.= [.0,1.] by TOPMETR:18 ;
A8: (L (0,1,(inf (dom c)),(sup (dom c)))) . 0 = ((((sup (dom c)) - (inf (dom c))) / (1 - 0)) * ()) + (inf (dom c)) by
.= inf (dom c) ;
A9: (L (0,1,(inf (dom c)),(sup (dom c)))) . 1 = ((((sup (dom c)) - (inf (dom c))) / (1 - 0)) * (1 - 0)) + (inf (dom c)) by
.= sup (dom c) ;
A10: p is continuous by ;
A11: p . 0 = the_first_point_of c by ;
A12: p . 1 = the_last_point_of c by ;
then the_first_point_of c, the_last_point_of c are_connected by ;
hence c * (L (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c by ; :: thesis: verum