( dom (Shift (f,h)) = (- h) ++ (dom f) & dom f = REAL ) by Def1, FUNCT_2:def 1;
then dom (Shift (f,h)) = REAL by MEASURE6:24;
hence Shift (f,h) is Function of REAL,REAL by FUNCT_2:def 1; :: thesis: verum