let f be Function; :: thesis: {} in sproduct f
A1: dom {} c= dom f by XBOOLE_1:2;
for x being set st x in dom {} holds
{} . x in f . x ;
hence {} in sproduct f by A1, Def9; :: thesis: verum