let K be Function; :: thesis: ( rng K is empty-membered iff for x being object holds K . x = {} )

hereby :: thesis: ( ( for x being object holds K . x = {} ) implies rng K is empty-membered )

assume A1: rng K is empty-membered ; :: thesis: for x being object holds K . b₂ = {}
let x be object ; :: thesis: K . b₁ = {}

per cases ( x in dom K or not x in dom K ) ;

suppose x in dom K ; :: thesis: K . b₁ = {}

hence K . x = {} by A1, FUNCT_1:3; :: thesis: verum

end;

suppose not x in dom K ; :: thesis: K . b₁ = {}

hence K . x = {} by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

assume A2: for x being object holds K . x = {} ; :: thesis: rng K is empty-membered

now :: thesis: for y being non empty set holds not y in rng K

assume ex y being non empty set st y in rng K ; :: thesis: contradiction
then consider y being non empty set such that
A3: y in rng K ;
ex a being object st
( a in dom K & y = K . a ) by A3, FUNCT_1:def 3;
hence contradiction by A2; :: thesis: verum

end;

hence rng K is empty-membered ; :: thesis: verum