let T be non empty TopStruct ; :: thesis: for c being with_endpoints Curve of T st dom c = [.0,1.] holds
c is Path of the_first_point_of c, the_last_point_of c
let c be with_endpoints Curve of T; :: thesis: ( dom c = [.0,1.] implies c is Path of the_first_point_of c, the_last_point_of c )
assume A1: dom c = [.0,1.] ; :: thesis: 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 f = c as parametrized-curve PartFunc of R^1,T by Th23;
consider S being SubSpace of R^1 , p being Function of S,T such that
A2: ( f = p & S = R^1 | (dom f) & p is continuous ) by Def4;
reconsider p = p as Function of I[01],T by A2, A1, BORSUK_1:40, FUNCT_2:def 1;
A3: S = I[01] by A2, A1, TOPMETR:19, TOPMETR:20;
A4: p . 0 = the_first_point_of c by A1, A2, XXREAL_2:25;
A5: p . 1 = the_last_point_of c by A2, A1, XXREAL_2:29;
then the_first_point_of c, the_last_point_of c are_connected by A2, A3, A4;
hence c is Path of the_first_point_of c, the_last_point_of c by A3, A4, A5, A2, BORSUK_2:def 2; :: thesis: verum