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

proof

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

end;

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