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