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

proof

assume A1: sproduct f = {{} } ; :: thesis: for x being set st x in dom f holds
f . x = {}
let x be set ; :: thesis: ( x in dom f implies f . x = {} )
assume A2: x in dom f ; :: thesis: f . x = {}
assume A3: f . x <> {} ; :: thesis: contradiction
consider y being Element of f . x;
x .--> y in sproduct f by A2, A3, Th76;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

assume A4: for x being set st x in dom f holds
f . x = {} ; :: thesis: sproduct f = {{} }

now

let x be set ; :: thesis: ( ( x in sproduct f implies x = {} ) & ( x = {} implies x in sproduct f ) )
thus ( x in sproduct f implies x = {} ) :: thesis: ( x = {} implies x in sproduct f )

proof

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

end;

thus ( x = {} implies x in sproduct f ) by Th66; :: thesis: verum

end;

hence sproduct f = {{} } by TARSKI:def 1; :: thesis: verum