let V be torsion-free Z_Module; :: thesis: for W being free finite-rank Subspace of V
for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
rank (W /\ (Lin {v})) = 1
let W be free finite-rank Subspace of V; :: thesis: for v being Vector of V st v <> 0. V & W /\ (Lin {v}) <> (0). V holds
rank (W /\ (Lin {v})) = 1
let v be Vector of V; :: thesis: ( v <> 0. V & W /\ (Lin {v}) <> (0). V implies rank (W /\ (Lin {v})) = 1 )
assume A1: ( v <> 0. V & W /\ (Lin {v}) <> (0). V ) ; :: thesis: rank (W /\ (Lin {v})) = 1
A2: rank (Lin {v}) = 1 by A1, LmRank0a;
A3: W /\ (Lin {v}) is Subspace of Lin {v} by ZMODUL01:105;
rank (W /\ (Lin {v})) <> 0
proof
assume rank (W /\ (Lin {v})) = 0 ; :: thesis: contradiction
then (Omega). (W /\ (Lin {v})) = (0). (W /\ (Lin {v})) by ZMODUL05:1
.= (0). V by ZMODUL01:51 ;
hence contradiction by A1; :: thesis: verum
end;
hence rank (W /\ (Lin {v})) = 1 by A3, NAT_1:25, ZMODUL05:2, A2; :: thesis: verum