for k being Nat st k in dom (Im f) holds
(Im f) . k = 0

proof

let k be Nat; :: thesis: ( k in dom (Im f) implies (Im f) . k = 0 )
assume k in dom (Im f) ; :: thesis: (Im f) . k = 0
then (Im f) . k = Im (f . k) by COMSEQ_3:def 4
.= 0 ;
hence (Im f) . k = 0 ; :: thesis: verum

end;

hence Im f is empty-yielding ; :: thesis: verum