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