:: deftheorem Def1 defines quasi_total FUNCT_2:def 1 :
for X, Y being set
for R being Relation of X,Y holds
( ( Y <> {} implies ( R is quasi_total iff X = dom R ) ) & ( not Y <> {} implies ( R is quasi_total iff R = {} ) ) );