let F be Field; :: thesis: for E being F -finite FieldExtension of F
for A being finite Subset of (VecSp (E,F)) st card A > dim (VecSp (E,F)) holds
A is linearly-dependent
let E be F -finite FieldExtension of F; :: thesis: for A being finite Subset of (VecSp (E,F)) st card A > dim (VecSp (E,F)) holds
A is linearly-dependent
let A be finite Subset of (VecSp (E,F)); :: thesis: ( card A > dim (VecSp (E,F)) implies A is linearly-dependent )
assume H: card A > dim (VecSp (E,F)) ; :: thesis: A is linearly-dependent
Y: VecSp (E,F) is finite-dimensional by FIELD_4:def 8;

now :: thesis: not A is linearly-independent

assume A is linearly-independent ; :: thesis: contradiction
then consider I being Basis of (VecSp (E,F)) such that
X: A c= I by VECTSP_7:19;
card I = dim (VecSp (E,F)) by Y, VECTSP_9:def 1;
hence contradiction by H, X, CARD_1:11, FIELD_5:3; :: thesis: verum

end;

hence A is linearly-dependent ; :: thesis: verum