set D = rng f;
f | k = f | (Seg k)
.= <*> (rng f) by RELAT_1:82 ;
hence f | k is empty ; :: thesis: verum