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

( 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