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