per cases ( Y = {} or Y <> {} ) ;
suppose A1: Y = {} ; :: thesis: ex b1 being PartFunc of X,Y st b1 is quasi_total
reconsider R = {} as PartFunc of X,Y by RELSET_1:12;
take R ; :: thesis: R is quasi_total
thus R is quasi_total by A1, Def1; :: thesis: verum
end;
suppose A2: Y <> {} ; :: thesis: ex b1 being PartFunc of X,Y st b1 is quasi_total
then consider f being Function such that
A3: X = dom f and
A4: rng f c= Y by FUNCT_1:8;
reconsider R = f as PartFunc of X,Y by A3, A4, RELSET_1:4;
take R ; :: thesis: R is quasi_total
thus R is quasi_total by A2, A3, Def1; :: thesis: verum
end;
end;