let f be non-empty Function; :: thesis: for X being set
for i being object st i in dom f holds
( f +* (i,X) is non-empty iff not X is empty )
let X be set ; :: thesis: for i being object st i in dom f holds
( f +* (i,X) is non-empty iff not X is empty )
let i be object ; :: thesis: ( i in dom f implies ( f +* (i,X) is non-empty iff not X is empty ) )
assume A1: i in dom f ; :: thesis: ( f +* (i,X) is non-empty iff not X is empty )

hereby :: thesis: ( not X is empty implies f +* (i,X) is non-empty )

assume A2: f +* (i,X) is non-empty ; :: thesis: not X is empty
i in dom (f +* (i,X)) by A1, FUNCT_7:30;
then (f +* (i,X)) . i <> {} by A2, FUNCT_1:def 9;
hence not X is empty by A1, FUNCT_7:31; :: thesis: verum

end;

assume A3: not X is empty ; :: thesis: f +* (i,X) is non-empty
for x being object st x in dom (f +* (i,X)) holds
not (f +* (i,X)) . x is empty

proof

let x be object ; :: thesis: ( x in dom (f +* (i,X)) implies not (f +* (i,X)) . x is empty )
assume A4: x in dom (f +* (i,X)) ; :: thesis: not (f +* (i,X)) . x is empty
A5: x in dom f by A4, FUNCT_7:30;
( x <> i implies (f +* (i,X)) . x = f . x ) by FUNCT_7:32;
hence not (f +* (i,X)) . x is empty by A5, FUNCT_1:def 9, A3, FUNCT_7:31; :: thesis: verum

end;

hence f +* (i,X) is non-empty by FUNCT_1:def 9; :: thesis: verum