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

proof

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

end;

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