let X, Y be set ; :: thesis: ( ( X <> {} & Y = {} ) iff product (X --> Y) = {} )

hereby :: thesis: ( product (X --> Y) = {} implies ( X <> {} & Y = {} ) )

assume ( X <> {} & Y = {} ) ; :: thesis: product (X --> Y) = {}
then rng (X --> Y) = {{}} by FUNCOP_1:8;
then {} in rng (X --> Y) by TARSKI:def 1;
hence product (X --> Y) = {} by CARD_3:26; :: thesis: verum

end;

assume product (X --> Y) = {} ; :: thesis: ( X <> {} & Y = {} )
hence ( X <> {} & Y = {} ) ; :: thesis: verum