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

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

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;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