let A be affinely-independent Subset of V; :: thesis: A is finite

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: A is finite

hence A is finite ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: A is finite

then consider v being VECTOR of V such that
v in A and
A1: ((- v) + A) \ {(0. V)} is linearly-independent by RLAFFIN1:def 4;
set vA = (- v) + A;
(((- v) + A) \ {(0. V)}) \/ {(0. V)} = ((- v) + A) \/ {(0. V)} by XBOOLE_1:39;
then A2: ( card ((- v) + A) = card A & (- v) + A c= (((- v) + A) \ {(0. V)}) \/ {(0. V)} ) by RLAFFIN1:7, XBOOLE_1:7;
((- v) + A) \ {(0. V)} is finite by A1, RLVECT_5:24;
hence A is finite by A2; :: thesis: verum

end;

end;