let F be Relation of X,Y; :: thesis: ( F is quasi_total implies F is total )
assume F is quasi_total ; :: thesis: F is total
hence X = dom F by Def1; :: according to PARTFUN1:def 2 :: thesis: verum