theorem Th17: :: RLAFFIN3:17

for V being RealLinearSpace
for v, w being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E