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