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

proof

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

end;

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

now :: thesis: for x being object holds
( ( x in sproduct f implies x = {} ) & ( x = {} implies x in sproduct f ) )

let x be object ; :: 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 object st y in dom g holds
g . y in f . y by Def9;
assume A8: x <> {} ; :: thesis: contradiction
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: verum

end;

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

end;

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