let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for A being Subset of V holds
( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )
let v be VECTOR of V; :: thesis: for A being Subset of V holds
( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )
let A be Subset of V; :: thesis: ( A \/ {v} is affinely-independent iff ( A is affinely-independent & ( v in A or not v in Affin A ) ) )
set Av = A \/ {v};
v in {v} by TARSKI:def 1;
then A1: v in A \/ {v} by XBOOLE_0:def 3;
A2: A c= A \/ {v} by XBOOLE_1:7;
thus ( A \/ {v} is affinely-independent implies ( A is affinely-independent & ( v in A or not v in Affin A ) ) ) by A1, A2, RLAFFIN1:58, RLAFFIN1:69, RLAFFIN1:82, ZFMISC_1:37; :: thesis: ( A is affinely-independent & ( v in A or not v in Affin A ) implies A \/ {v} is affinely-independent )
assume that
A4: A is affinely-independent and
A5: ( v in A or not v in Affin A ) ; :: thesis: A \/ {v} is affinely-independent

per cases ( v in A or ( not v in Affin A & not v in A ) ) by A5;

suppose v in A ; :: thesis: A \/ {v} is affinely-independent

hence A \/ {v} is affinely-independent by A4, ZFMISC_1:46; :: thesis: verum

end;

suppose A6: ( not v in Affin A & not v in A ) ; :: thesis: A \/ {v} is affinely-independent

consider I being affinely-independent Subset of V such that
A7: A c= I and
A8: I c= A \/ {v} and
A9: Affin I = Affin (A \/ {v}) by A2, A4, RLAFFIN1:60;
assume A10: not A \/ {v} is affinely-independent ; :: thesis: contradiction
not v in I

proof

assume v in I ; :: thesis: contradiction
then {v} c= I by ZFMISC_1:37;
hence contradiction by A7, A10, RLAFFIN1:43, XBOOLE_1:8; :: thesis: verum

end;

then A11: I c= (A \/ {v}) \ {v} by A8, ZFMISC_1:40;
(A \/ {v}) \ {v} = A by A6, ZFMISC_1:141;
then ( A \/ {v} c= Affin (A \/ {v}) & I = A ) by A7, A11, RLAFFIN1:49, XBOOLE_0:def 10;
hence contradiction by A1, A6, A9; :: thesis: verum

end;

end;