let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T
for t1, t2 being Point of T st c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 & t1,t2 are_connected holds
( t1 = the_first_point_of c & t2 = the_last_point_of c )
let c be with_endpoints Curve of T; :: thesis: for t1, t2 being Point of T st c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 & t1,t2 are_connected holds
( t1 = the_first_point_of c & t2 = the_last_point_of c )
let t1, t2 be Point of T; :: thesis: ( c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 & t1,t2 are_connected implies ( t1 = the_first_point_of c & t2 = the_last_point_of c ) )
assume A1: ( c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 & t1,t2 are_connected ) ; :: thesis: ( t1 = the_first_point_of c & t2 = the_last_point_of c )
A2: inf (dom c) <= sup (dom c) by XXREAL_2:40;
A3: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
A4: 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 ;
A5: (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) ;
A6: (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) ;
reconsider p = c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) as Path of t1,t2 by A1;
A7: p . 0 = the_first_point_of c by A5, A3, A4, FUNCT_1:13;
p . 1 = the_last_point_of c by A6, A3, A4, FUNCT_1:13;
hence ( t1 = the_first_point_of c & t2 = the_last_point_of c ) by A7, A1, BORSUK_2:def 2; :: thesis: verum