let V be RealLinearSpace; :: thesis: for Av being finite Subset of V

for x being object

for E being Enumeration of Av holds len (x |-- E) = card Av

let Av be finite Subset of V; :: thesis: for x being object

for E being Enumeration of Av holds len (x |-- E) = card Av

let x be object ; :: 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

for x being object

for E being Enumeration of Av holds len (x |-- E) = card Av

let Av be finite Subset of V; :: thesis: for x being object

for E being Enumeration of Av holds len (x |-- E) = card Av

let x be object ; :: 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