let f be non-empty Function; 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 ; 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 ; ( i in dom f implies ( f +* (i,X) is non-empty iff not X is empty ) )
assume A1:
i in dom f
; ( f +* (i,X) is non-empty iff not X is empty )
assume A3:
not X is empty
; 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 ;
( x in dom (f +* (i,X)) implies not (f +* (i,X)) . x is empty )
assume A4:
x in dom (f +* (i,X))
;
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;
verum
end;
hence
f +* (i,X) is non-empty
by FUNCT_1:def 9; verum