for NT being NTopSpace
for f being Function of NT,FMT_R^1 holds NTop2Top f is Function of (NTop2Top NT),R^1 by FINTOPO7:24;