let T be TopStruct ; :: thesis: for c being Curve of T holds
( dom c c= REAL & rng c c= [#] T )
let c be Curve of T; :: thesis: ( dom c c= REAL & rng c c= [#] T )
reconsider f = c as parametrized-curve PartFunc of R^1,T by Th23;
( dom f c= [#] R^1 & rng f c= [#] T ) ;
hence ( dom c c= REAL & rng c c= [#] T ) by TOPMETR:17; :: thesis: verum