let x be set ; :: thesis: for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av holds len (x |-- E) = card Av
let V be RealLinearSpace; :: thesis: for Av being finite Subset of V
for E being Enumeration of Av holds len (x |-- E) = card Av
let Av be finite Subset of V; :: thesis: for E being Enumeration of Av holds len (x |-- E) = card Av
let E be Enumeration of Av; :: thesis: len (x |-- E) = card Av
rng E = Av by Def1;
then len E = card Av by FINSEQ_4:62;
hence len (x |-- E) = card Av by FINSEQ_2:33; :: thesis: verum