let f be Relation of X,Y; :: thesis: ( f is total implies f is quasi_total )
assume A1: dom f = X ; :: according to PARTFUN1:def 2 :: thesis: f is quasi_total

per cases ( Y <> {} or Y = {} ) ;
:: according to FUNCT_2:def 1

case Y <> {} ; :: thesis: X = dom f

thus X = dom f by A1; :: thesis: verum

end;

case Y = {} ; :: thesis: f = {}

hence f = {} ; :: thesis: verum

end;

end;