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 quasi_total by FUNCT_2:def 1; :: thesis: verum

.= REAL /\ (dom (Shift (f,(- (h / 2))))) by FUNCT_2:def 1

.= REAL /\ REAL by FUNCT_2:def 1

.= REAL ;

hence cD (f,h) is quasi_total by FUNCT_2:def 1; :: thesis: verum