:: deftheorem defines |-- RLAFFIN3:def 2 :
for V being RealLinearSpace
for Av being finite Subset of V
for E being Enumeration of Av
for x being object holds x |-- E = (x |-- Av) * E;