let T be non empty TopStruct ; :: thesis: for c being Curve of T
for r1, r2 being Real holds c | [.r1,r2.] is Curve of T
let c be Curve of T; :: thesis: for r1, r2 being Real holds c | [.r1,r2.] is Curve of T
let r1, r2 be Real; :: thesis: c | [.r1,r2.] is Curve of T
reconsider f = c as parametrized-curve PartFunc of R^1,T by Th23;
set f1 = f | [.r1,r2.];
reconsider A = dom f as interval Subset of REAL by Def4;
reconsider B = [.r1,r2.] as interval Subset of REAL ;
A1: A /\ B is interval Subset of REAL ;
then A2: dom (f | [.r1,r2.]) is interval Subset of REAL by RELAT_1:61;
consider S being SubSpace of R^1 , g being Function of S,T such that
A3: ( f = g & S = R^1 | (dom f) & g is continuous ) by Def4;
reconsider A0 = dom f as Subset of R^1 ;
A4: [#] S = A0 by A3, PRE_TOPC:def 5;
reconsider K0 = (dom f) /\ [.r1,r2.] as Subset of S by A4, XBOOLE_1:17;
reconsider g1 = g | K0 as Function of (S | K0),T by PRE_TOPC:9;
A5: g1 is continuous by A3, TOPMETR:7;
A6: g1 = (f | (dom f)) | [.r1,r2.] by A3, RELAT_1:71
.= f | [.r1,r2.] ;
A7: (dom f) /\ [.r1,r2.] = dom (f | [.r1,r2.]) by RELAT_1:61;
reconsider K1 = K0 as Subset of (R^1 | A0) by A3;
reconsider D1 = dom (f | [.r1,r2.]) as Subset of R^1 by A1, RELAT_1:61, TOPMETR:17;
S | K0 = R^1 | D1 by A3, A7, PRE_TOPC:7, XBOOLE_1:17;
then reconsider f1 = f | [.r1,r2.] as parametrized-curve PartFunc of R^1,T by A2, A5, A6, Def4;
c | [.r1,r2.] = f1 ;
hence c | [.r1,r2.] is Curve of T by Th20; :: thesis: verum