set C = { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } ;
for x being object st x in { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } holds
x in PFuncs (REAL,([#] T))

proof

let x be object ; :: thesis: ( x in { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } implies x in PFuncs (REAL,([#] T)) )
assume x in { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } ; :: thesis: x in PFuncs (REAL,([#] T))
then ex f being Element of PFuncs (REAL,([#] T)) st
( x = f & f is parametrized-curve PartFunc of R^1,T ) ;
hence x in PFuncs (REAL,([#] T)) ; :: thesis: verum

end;

hence { f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T } is Subset of (PFuncs (REAL,([#] T))) by TARSKI:def 3; :: thesis: verum