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)

let A be affinely-independent Subset of V; :: thesis: card A <= 1 + (dim V)

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

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