let f be PartFunc of X,D; :: thesis: ( f is quasi_total implies f is total )
assume f is quasi_total ; :: thesis: f is total
then dom f = X by Def1;
hence f is total by PARTFUN1:def 2; :: thesis: verum