len f <= ((len f) + n) + 0 by NAT_1:11;
then (len f) - ((len f) + n) <= 0 by XREAL_1:20;
then (len f) -' ((len f) + n) = 0 by XREAL_0:def 2;
then len (f /^ ((dom f) + n)) = 0 by Def2;
hence f /^ ((dom f) + n) is empty ; :: thesis: verum