per cases ( Y = {} or Y <> {} ) ;

suppose A1: Y = {} ; :: thesis: ex b₁ being PartFunc of X,Y st b₁ 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 b₁ being PartFunc of X,Y st b₁ 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;