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

suppose Y = {} ; :: thesis: for b₁ being PartFunc of X,Y st b₁ = f * g holds
b₁ is quasi_total

hence for b₁ being PartFunc of X,Y st b₁ = f * g holds
b₁ is quasi_total ; :: thesis: verum

end;

suppose A1: Y <> {} ; :: thesis: for b₁ being PartFunc of X,Y st b₁ = f * g holds
b₁ is quasi_total

then dom f = X by Def1;
then dom (f * g) = g " X by RELAT_1:147
.= dom g by RELSET_1:22
.= X by Th51 ;
hence for b₁ being PartFunc of X,Y st b₁ = f * g holds
b₁ is quasi_total by A1, Def1; :: thesis: verum

end;

end;