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