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

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

case ( Y = {} implies X = {} ) ; :: thesis: X = dom f

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

end;

case ( Y = {} & X <> {} ) ; :: thesis: f = {}

hence f = {} ; :: thesis: verum

end;

end;