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