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

let A be affinely-independent Subset of V; :: thesis: ( card A = (dim V) + 1 iff Affin A = [#] V )
A1: 0. V in [#] V ;
A2: A c= Affin A by RLAFFIN1:49;
hereby :: thesis: ( Affin A = [#] V implies card A = (dim V) + 1 )
assume A3: card A = (dim V) + 1 ; :: thesis:
then not A is empty ;
then consider v being VECTOR of V such that
A4: v in A and
A5: ((- v) + A) \ {(0. V)} is linearly-independent by RLAFFIN1:def 4;
set vA = (- v) + A;
reconsider vA = (- v) + A as finite Subset of V ;
(- v) + v in { ((- v) + w) where w is Element of V : w in A } by A4;
then A6: (- v) + v in vA by RUSUB_4:def 8;
A7: ( card vA = card A & card {(0. V)} = 1 ) by ;
(- v) + v = 0. V by RLVECT_1:5;
then vA = (vA \ {(0. V)}) \/ {(0. V)} by ;
then A8: card A = (card (vA \ {(0. V)})) + 1 by ;
dim (Lin (vA \ {(0. V)})) = card (vA \ {(0. V)}) by ;
then (Omega). V = (Omega). (Lin (vA \ {(0. V)})) by
.= Lin (vA \ {(0. V)}) by RLSUB_1:def 4 ;
then RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = Lin (vA \ {(0. V)}) by RLSUB_1:def 4;
then A9: [#] V = the carrier of (Lin vA) by Lm2;
then v in Lin vA ;
hence [#] V = v + (Lin vA) by
.= v + (Up (Lin vA)) by RUSUB_4:30
.= Affin A by ;
:: thesis: verum
end;
assume A10: Affin A = [#] V ; :: thesis: card A = (dim V) + 1
then not A is empty ;
then consider v being VECTOR of V such that
A11: v in A and
A12: ((- v) + A) \ {(0. V)} is linearly-independent by RLAFFIN1:def 4;
set vA = (- v) + A;
reconsider vA = (- v) + A as finite Subset of V ;
[#] V = v + (Up (Lin vA)) by
.= v + (Lin vA) by RUSUB_4:30 ;
then [#] (Lin vA) = the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by
.= the carrier of () by RLSUB_1:def 4 ;
then Lin vA = (Omega). V by RLSUB_1:30
.= RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by RLSUB_1:def 4 ;
then RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = Lin (vA \ {(0. V)}) by Lm2;
then A13: vA \ {(0. V)} is Basis of V by ;
(- v) + v in { ((- v) + w) where w is Element of V : w in A } by A11;
then A14: (- v) + v in vA by RUSUB_4:def 8;
(- v) + v = 0. V by RLVECT_1:5;
then A15: vA = (vA \ {(0. V)}) \/ {(0. V)} by ;
( card vA = card A & card {(0. V)} = 1 ) by ;
hence card A = (card (vA \ {(0. V)})) + 1 by
.= (dim V) + 1 by ;
:: thesis: verum