let f be non-empty Function; :: thesis: for X being set
for i being object st i in dom f holds
( product (f +* (i,X)) = {} iff X is empty )
let X be set ; :: thesis: for i being object st i in dom f holds
( product (f +* (i,X)) = {} iff X is empty )
let i be object ; :: thesis: ( i in dom f implies ( product (f +* (i,X)) = {} iff X is empty ) )
assume A1: i in dom f ; :: thesis: ( product (f +* (i,X)) = {} iff X is empty )
then A2: i in dom (f +* (i,X)) by FUNCT_7:30;

hereby :: thesis: ( X is empty implies product (f +* (i,X)) = {} )

assume product (f +* (i,X)) = {} ; :: thesis: X is empty
then not f +* (i,X) is non-empty ;
hence X is empty by A1, Th35; :: thesis: verum

end;

assume X is empty ; :: thesis: product (f +* (i,X)) = {}
then (f +* (i,X)) . i = {} by A1, FUNCT_7:31;
then {} in rng (f +* (i,X)) by A2, FUNCT_1:def 3;
hence product (f +* (i,X)) = {} by CARD_3:26; :: thesis: verum