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