let f be Function; :: thesis:
thus ( sproduct f = {{}} implies for x being object st x in dom f holds
f . x = {} ) :: thesis:

end;

assume x in sproduct f ; :: thesis:
then consider g being Function such that
A5: x = g and
A6: dom g c= dom f and
A7: for y being object st y in dom g holds
g . y in f . y by Def9;
assume A8: x <> {} ; :: thesis:
set y = the Element of dom g;
A9: f . the Element of dom g <> {} by A5, A7, A8;
the Element of dom g in dom f by A5, A6, A8;
hence contradiction by A4, A9; :: thesis:

end;

end;