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

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

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

assume
product (X --> Y) = {}
; :: thesis: ( 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;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

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