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 ;
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 ;
then card (vA \ {(0. V)}) <= dim V by RLVECT_5:28;
then A4: card ((vA \ {(0. V)}) \/ {(0. V)}) <= 1 + (dim V) by ;
(vA \ {(0. V)}) \/ {(0. V)} = vA \/ {(0. V)} by XBOOLE_1:39;
then card A <= card ((vA \ {(0. V)}) \/ {(0. V)}) by ;
hence card A <= 1 + (dim V) by ; :: thesis: verum
end;
end;