let T be non empty TopStruct ; 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; ( 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.]
; 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; verum