let V be finite-dimensional RealLinearSpace; :: thesis: for A being affinely-independent Subset of V holds card A <= 1 + (dim V)
let A be affinely-independent Subset of V; :: thesis: card A <= 1 + (dim V)

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

suppose A is empty ; :: thesis: card A <= 1 + (dim V)

hence card A <= 1 + (dim V) ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: card A <= 1 + (dim V)

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)} misses {(0. V)} by XBOOLE_1:79;
then A2: ( card {(0. V)} = 1 & card ((((- v) + A) \ {(0. V)}) \/ {(0. V)}) = (card (((- v) + A) \ {(0. V)})) + (card {(0. V)}) ) by CARD_2:40, CARD_2:42;
A3: card ((- v) + A) = card A by RLAFFIN1:7;
reconsider vA = (- v) + A as finite set ;
card (vA \ {(0. V)}) = dim (Lin (((- v) + A) \ {(0. V)})) by A1, RLVECT_5:29;
then card (vA \ {(0. V)}) <= dim V by RLVECT_5:28;
then A4: card ((vA \ {(0. V)}) \/ {(0. V)}) <= 1 + (dim V) by A2, XREAL_1:7;
(vA \ {(0. V)}) \/ {(0. V)} = vA \/ {(0. V)} by XBOOLE_1:39;
then card A <= card ((vA \ {(0. V)}) \/ {(0. V)}) by A3, NAT_1:43, XBOOLE_1:7;
hence card A <= 1 + (dim V) by A4, XXREAL_0:2; :: thesis: verum

end;

end;