let T be TopStruct ; :: thesis: for c being Curve of T holds c is parametrized-curve PartFunc of R^1,T
let c be Curve of T; :: thesis: c is parametrized-curve PartFunc of R^1,T
c in { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } ;
then consider f being Element of PFuncs (REAL,([#] T)) such that
A1: ( c = f & f is parametrized-curve PartFunc of R^1,T ) ;
thus c is parametrized-curve PartFunc of R^1,T by A1; :: thesis: verum