dom (bD f,h) = (dom (Shift f,(- h))) /\ (dom f) by VALUED_1:12
.= REAL /\ (dom f) by FUNCT_2:def 1
.= REAL /\ REAL by FUNCT_2:def 1
.= REAL ;
hence bD f,h is Function of REAL ,REAL by FUNCT_2:def 1; :: thesis: verum