A2: len (Incr v) = card (rng v) by Def25;
assume Incr v is empty ; :: thesis: contradiction
then rng v = {} by A2;
hence contradiction ; :: thesis: verum