dom f = X by FUNCT_2:def 1;
then A1: dom |[f]| = X by Def1;
rng |[f]| c= the carrier of (TOP-REAL 1) ;
hence |[f]| is Function of X,(TOP-REAL 1) by A1, FUNCT_2:2; :: thesis: verum