let T be TopStruct ; :: thesis: for f being PartFunc of R^1,T st f = {} holds
f is parametrized-curve
let f be PartFunc of R^1,T; :: thesis: ( f = {} implies f is parametrized-curve )
assume A1: f = {} ; :: thesis: f is parametrized-curve
reconsider f = f as PartFunc of R^1,T ;
dom f = {} by A1;
then A2: dom f c= REAL ;
reconsider A = {} as Subset of R^1 by XBOOLE_1:2;
reconsider S = R^1 | A as SubSpace of R^1 ;
reconsider g = f as Relation of ([#] S),([#] T) by A1;
A3: A = dom g ;
reconsider g = g as Function of S,T ;
for P1 being Subset of T st P1 is closed holds
g " P1 is closed ;
then g is continuous by PRE_TOPC:def 6;
hence f is parametrized-curve by A3, A2; :: thesis: verum