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 )

for x being object st x in dom (f +* (i,X)) holds

not (f +* (i,X)) . x is empty

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 A3:
not X is empty
; :: thesis: 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;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

for x being object st x in dom (f +* (i,X)) holds

not (f +* (i,X)) . x is empty

proof

hence
f +* (i,X) is non-empty
by FUNCT_1:def 9; :: thesis: verum
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;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