let V be torsion-free Z_Module; :: thesis: for W1, W2 being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V holds
rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2)
let W1, W2 be free finite-rank Subspace of V; :: thesis: for v being Vector of V st v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V holds
rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2)
let v be Vector of V; :: thesis: ( v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V implies rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2) )
assume A1: ( v <> 0. V & W1 /\ (Lin {v}) = (0). V & (W1 + W2) /\ (Lin {v}) = (0). V ) ; :: thesis: rank ((W1 + (Lin {v})) /\ W2) = rank (W1 /\ W2)
for u being Vector of V st u in W1 /\ W2 holds
u in (W1 + (Lin {v})) /\ W2 then W1 /\ W2 is Subspace of (W1 + (Lin {v})) /\ W2 by ZMODUL01:44;
then A2: rank ((W1 + (Lin {v})) /\ W2) >= rank (W1 /\ W2) by ZMODUL05:2;
assume AS: rank ((W1 + (Lin {v})) /\ W2) <> rank (W1 /\ W2) ; :: thesis: contradiction
ex u being Vector of V st
( u in (W1 + (Lin {v})) /\ W2 & not u in W1 /\ W2 ) then consider u being Vector of V such that
A4: ( u in (W1 + (Lin {v})) /\ W2 & not u in W1 /\ W2 ) ;
u in W1 + (Lin {v}) by A4, ZMODUL01:94;
then consider u1, u2 being Vector of V such that
A5: ( u1 in W1 & u2 in Lin {v} & u = u1 + u2 ) by ZMODUL01:92;
A6: u in W2 by A4, ZMODUL01:94;
A7: u2 <> 0. V by A4, A5, A6, ZMODUL01:94;
A8: - u1 in W1 by A5, ZMODUL01:38;
u - u1 = u2 + (u1 - u1) by RLVECT_1:28, A5
.= u2 + (0. V) by RLVECT_1:15
.= u2 ;
then u2 in W1 + W2 by A6, A8, ZMODUL01:92;
hence contradiction by A1, A7, ZMODUL02:66, A5, ZMODUL01:94; :: thesis: verum