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;