for l being Element of NAT holds NIC (a :=len f),l = {(succ l)} by Th82;
hence JUMP (a :=len f) is empty by Lm6; :: thesis: verum