let T be non empty TopStruct ; :: thesis: for r1, r2 being real number
for t1, t2 being Point of T
for p1 being Path of t1,t2 st t1,t2 are_connected & r1 < r2 holds
p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T
let r1, r2 be real number ; :: thesis: for t1, t2 being Point of T
for p1 being Path of t1,t2 st t1,t2 are_connected & r1 < r2 holds
p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T
let t1, t2 be Point of T; :: thesis: for p1 being Path of t1,t2 st t1,t2 are_connected & r1 < r2 holds
p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T
let p1 be Path of t1,t2; :: thesis: ( t1,t2 are_connected & r1 < r2 implies p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T )
assume A1: t1,t2 are_connected ; :: thesis: ( not r1 < r2 or p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T )
assume A2: r1 < r2 ; :: thesis: p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T
then A3: L[01] (r1,r2,0,1) is continuous Function of (Closed-Interval-TSpace (r1,r2)),(Closed-Interval-TSpace (0,1)) by BORSUK_6:34;
A4: ( p1 is continuous & p1 . 0 = t1 & p1 . 1 = t2 ) by A1, BORSUK_2:def 2;
set c = p1 * (L[01] (r1,r2,0,1));
rng (L[01] (r1,r2,0,1)) c= [#] (Closed-Interval-TSpace (0,1)) by RELAT_1:def 19;
then rng (L[01] (r1,r2,0,1)) c= dom p1 by FUNCT_2:def 1, TOPMETR:20;
then dom (p1 * (L[01] (r1,r2,0,1))) = dom (L[01] (r1,r2,0,1)) by RELAT_1:27;
then dom (p1 * (L[01] (r1,r2,0,1))) = [#] (Closed-Interval-TSpace (r1,r2)) by FUNCT_2:def 1;
then A5: dom (p1 * (L[01] (r1,r2,0,1))) = [.r1,r2.] by A2, TOPMETR:18;
A6: rng (p1 * (L[01] (r1,r2,0,1))) c= [#] T ;
then reconsider c = p1 * (L[01] (r1,r2,0,1)) as PartFunc of R^1,T by A5, RELSET_1:4, TOPMETR:17;
set S = R^1 | (dom c);
dom c = [#] (R^1 | (dom c)) by PRE_TOPC:def 5;
then reconsider g = c as Function of (R^1 | (dom c)),T by A6, FUNCT_2:2;
A7: R^1 | (dom c) = Closed-Interval-TSpace (r1,r2) by A2, A5, TOPMETR:19;
reconsider p2 = p1 as Function of (Closed-Interval-TSpace (0,1)),T by TOPMETR:20;
g is continuous by A4, A7, A3, TOPMETR:20, TOPS_2:46;
then c is parametrized-curve by A5, Def4;
then reconsider c = c as Curve of T by Th20;
( dom c is left_end & dom c is right_end ) by A2, A5, XXREAL_2:33;
then ( c is with_first_point & c is with_last_point ) by Def6, Def7;
hence p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T ; :: thesis: verum