let M be finite-degree Matroid; :: thesis: for A being Subset of M
for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds
e in Span (A \/ {f})
let A be Subset of M; :: thesis: for f, e being Element of M st f nin Span A & f in Span (A \/ {e}) holds
e in Span (A \/ {f})
let f, e be Element of M; :: thesis: ( f nin Span A & f in Span (A \/ {e}) implies e in Span (A \/ {f}) )
assume that
Z1: f nin Span A and
Z2: f in Span (A \/ {e}) ; :: thesis: e in Span (A \/ {f})
A3: ( Rnk A <> Rnk (A \/ {f}) & Rnk ((A \/ {e}) \/ {f}) = Rnk (A \/ {e}) ) by Z1, Z2, SPAN;
( Rnk A <= Rnk (A \/ {f}) & Rnk (A \/ {f}) <= (Rnk A) + 1 ) by R4;
then A4: Rnk (A \/ {f}) = (Rnk A) + 1 by A3, NAT_1:9;
A5: ( A \/ {f} c= (A \/ {f}) \/ {e} & (A \/ {f}) \/ {e} = A \/ ({f} \/ {e}) & (A \/ {e}) \/ {f} = A \/ ({e} \/ {f}) ) by XBOOLE_1:4, XBOOLE_1:7;
then ( Rnk (A \/ {f}) <= Rnk (A \/ {e}) & Rnk (A \/ {e}) <= (Rnk A) + 1 ) by A3, R4;
then Rnk (A \/ {f}) = Rnk ((A \/ {f}) \/ {e}) by A3, A4, A5, XXREAL_0:1;
hence e in Span (A \/ {f}) by SPAN; :: thesis: verum