let T be TopStruct ; :: thesis: for f being parametrized-curve PartFunc of R^1,T holds f is Curve of T
let f be parametrized-curve PartFunc of R^1,T; :: thesis: f is Curve of T
reconsider f1 = f as Element of PFuncs (REAL,([#] T)) by PARTFUN1:45, TOPMETR:17;
f1 in Curves T ;
hence f is Curve of T ; :: thesis: verum