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;

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

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
X is empty
; :: thesis: 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;then not f +* (i,X) is non-empty ;

hence X is empty by A1, Th35; :: thesis: verum

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