dom (bD (f,h)) = (dom (Shift (f,(- h)))) /\ (dom f) by VFUNCT_1:def 2
.= the carrier of V /\ (dom f) by FUNCT_2:def 1
.= the carrier of V /\ the carrier of V by FUNCT_2:def 1
.= the carrier of V ;
hence bD (f,h) is quasi_total by FUNCT_2:def 1; :: thesis: verum