let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T holds the_first_point_of c, the_last_point_of c are_connected
let c be with_endpoints Curve of T; :: thesis: the_first_point_of c, the_last_point_of c are_connected
set t1 = the_first_point_of c;
set t2 = the_last_point_of c;
reconsider f = 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: ( f = g & S = R^1 | (dom f) & g is continuous ) by Def4;
set r1 = inf (dom c);
set r2 = sup (dom c);
set p = g * (L[01] (0,1,(inf (dom c)),(sup (dom c))));
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;
rng (L[01] (0,1,(inf (dom c)),(sup (dom c)))) c= [#] (Closed-Interval-TSpace ((inf (dom c)),(sup (dom c)))) by RELAT_1:def 19;
then rng (L[01] (0,1,(inf (dom c)),(sup (dom c)))) c= [.(inf (dom c)),(sup (dom c)).] by A2, TOPMETR:18;
then rng (L[01] (0,1,(inf (dom c)),(sup (dom c)))) c= dom c by Th27;
then dom (g * (L[01] (0,1,(inf (dom c)),(sup (dom c))))) = dom (L[01] (0,1,(inf (dom c)),(sup (dom c)))) by A1, RELAT_1:27;
then A4: dom (g * (L[01] (0,1,(inf (dom c)),(sup (dom c))))) = [#] (Closed-Interval-TSpace (0,1)) by FUNCT_2:def 1;
rng (g * (L[01] (0,1,(inf (dom c)),(sup (dom c))))) c= [#] T ;
then reconsider p = g * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) as Function of I[01],T by A4, FUNCT_2:2, TOPMETR:20;
dom f = [.(inf (dom c)),(sup (dom c)).] by Th27;
then S = Closed-Interval-TSpace ((inf (dom c)),(sup (dom c))) by A1, A2, TOPMETR:19;
then A5: p is continuous by A1, A3, TOPMETR:20, TOPS_2:46;
dom p = [.0,1.] by A4, TOPMETR:18;
then A6: ( 0 in dom p & 1 in dom p ) by XXREAL_1:1;
A7: (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) ;
A8: (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) ;
A9: p . 0 = the_first_point_of c by A1, A7, A6, FUNCT_1:12;
p . 1 = the_last_point_of c by A1, A8, A6, FUNCT_1:12;
hence the_first_point_of c, the_last_point_of c are_connected by A5, A9; :: thesis: verum