for V being RealLinearSpace
for Av being finite Subset of V
for x being object
for E being Enumeration of Av holds len (x |-- E) = card Av