let R be Relation of A,U; :: thesis: ( R is quasi_total implies R is total )
assume R is quasi_total ; :: thesis: R is total
then dom R = A by FUNCT_2:def 1;
hence R is total by PARTFUN1:def 2; :: thesis: verum