for m being non zero Nat
for f being PartFunc of (REAL m),(REAL 1) ex f0 being PartFunc of (REAL m),REAL st f = <>* f0