dom (cD (f,h)) =
(dom (Shift (f,(((2 * (1. F)) ") * h)))) /\ (dom (Shift (f,(- (((2 * (1. F)) ") * h)))))
by VFUNCT_1:def 2

.= the carrier of V /\ (dom (Shift (f,(- (((2 * (1. F)) ") * h))))) by FUNCT_2:def 1

.= the carrier of V /\ the carrier of V by FUNCT_2:def 1

.= the carrier of V ;

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

.= the carrier of V /\ (dom (Shift (f,(- (((2 * (1. F)) ") * h))))) by FUNCT_2:def 1

.= the carrier of V /\ the carrier of V by FUNCT_2:def 1

.= the carrier of V ;

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