for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite Function