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

suppose Y = {} ; :: thesis: f * g is quasi_total PartFunc of X,Y

hence f * g is quasi_total PartFunc of X,Y ; :: thesis: verum

end;

suppose S: Y <> {} ; :: thesis: f * g is quasi_total PartFunc of X,Y

then dom f = X by Def1;
then dom (f * g) = g " X by RELAT_1:182
.= dom g by RELSET_1:38
.= X by Th67 ;
hence f * g is quasi_total PartFunc of X,Y by Def1, S; :: thesis: verum

end;

end;