per cases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; :: thesis: for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
hence for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total ; :: thesis: verum
end;
suppose A1: Y <> {} ; :: thesis: for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total
dom f = Y by Th51;
then dom (f * g) = g " Y by RELAT_1:147
.= dom g by RELSET_1:22
.= X by A1, Def1 ;
hence for b1 being PartFunc of X,Y st b1 = f * g holds
b1 is quasi_total by A1, Def1; :: thesis: verum
end;
end;