for A being finite Subset of VAR holds A, code A are_equipotent by Lm8;