let M be finite-degree Matroid; :: thesis: for A being Subset of M holds Rnk (Span A) = Rnk A
let A be Subset of M; :: thesis: Rnk (Span A) = Rnk A
consider Ca being independent Subset of M such that
A1: Ca c= A and
A2: card Ca = Rnk A by Th18;
A c= Span A by Th31;
then Ca c= Span A by A1;
then consider C being independent Subset of M such that
A3: Ca c= C and
A4: C is_maximal_independent_in Span A by Th14;

now :: thesis: not C c/= Ca

assume C c/= Ca ; :: thesis: contradiction
then consider x being object such that
A5: x in C and
A6: x nin Ca ;
C c= Span A by A4;
then x in Span A by A5;
then consider e being Element of M such that
A7: x = e and
A8: e is_dependent_on A ;
{e} c= C by A5, A7, ZFMISC_1:31;
then Ca \/ {e} c= C by A3, XBOOLE_1:8;
then reconsider Ce = Ca \/ {e} as independent Subset of M by Th3;
Ce c= A \/ {e} by A1, XBOOLE_1:9;
then consider D being independent Subset of M such that
A9: Ce c= D and
A10: D is_maximal_independent_in A \/ {e} by Th14;
card Ca = Rnk (A \/ {e}) by A2, A8
.= card D by A10, Th19 ;
then A11: card Ce <= card Ca by A9, NAT_1:43;
card Ca <= card Ce by NAT_1:43, XBOOLE_1:7;
then card Ca = card Ce by A11, XXREAL_0:1;
then Ca = Ce by CARD_2:102, XBOOLE_1:7;
then e nin {e} by A6, A7, XBOOLE_0:def 3;
hence contradiction by TARSKI:def 1; :: thesis: verum

end;

then C = Ca by A3;
hence Rnk (Span A) = Rnk A by A2, A4, Th19; :: thesis: verum