set I = the Basis of V;
card the Basis of V > 0

proof

assume card the Basis of V <= 0 ; :: thesis: contradiction
then the Basis of V = {} the carrier of V ;
then Lin the Basis of V = (0). V by ZMODUL02:67;
then (Omega). V = (0). V by VECTSP_7:def 3;
hence contradiction ; :: thesis: verum

end;

then not the Basis of V is empty ;
then consider v being object such that
A1: v in the Basis of V by XBOOLE_0:def 1;
reconsider v = v as Vector of V by A1;
( V is Submodule of V & the Basis of V is linearly-independent & (Omega). V = Lin the Basis of V ) by ZMODUL01:32, VECTSP_7:def 3;
then ( (Omega). V = (Lin ( the Basis of V \ {v})) + (Lin {v}) & (Lin ( the Basis of V \ {v})) /\ (Lin {v}) = (0). V & Lin ( the Basis of V \ {v}) is free & Lin {v} is free & v <> 0. V ) by A1, ZMODUL06:24;
then A6: not v is torsion by ZMODUL06:def 3;
reconsider pp = p as Element of INT.Ring ;
assume VectQuot (V,(p (*) V)) is trivial ; :: thesis: contradiction
then (ZQMorph (V,(p (*) V))) . v = 0. (VectQuot (V,(p (*) V)))
.= zeroCoset (V,(p (*) V)) by VECTSP10:def 6
.= the carrier of (p (*) V) ;
then v + (p (*) V) = the carrier of (p (*) V) by defMophVW;
then v in p (*) V by ZMODUL01:63;
then consider u being Vector of V such that
A3: v = pp * u ;
( the Basis of V \ {v}) \/ {v} = the Basis of V \/ {v} by XBOOLE_1:39
.= the Basis of V by A1, XBOOLE_1:12, ZFMISC_1:31 ;
then Lin the Basis of V = (Lin ( the Basis of V \ {v})) + (Lin {v}) by ZMODUL02:72;
then consider u1, u2 being Vector of V such that
B4: ( u1 in Lin ( the Basis of V \ {v}) & u2 in Lin {v} & u = u1 + u2 ) by ZMODUL01:92, ZMODUL03:14;
B5: v = (pp * u1) + (pp * u2) by A3, B4, VECTSP_1:def 14;
B6: pp * u1 in Lin ( the Basis of V \ {v}) by B4, ZMODUL01:37;
B7: pp * u2 in Lin {v} by B4, ZMODUL01:37;
consider iu2 being Element of INT.Ring such that
B8: u2 = iu2 * v by B4, ZMODUL06:19;
B9: pp * u2 = (pp * iu2) * v by B8, VECTSP_1:def 16;
B10: V is_the_direct_sum_of Lin ( the Basis of V \ {v}), Lin {v} by A1, ZMODUL04:33;
B11: v = ((1. INT.Ring) * v) + (0. V) ;
B12: v in Lin {v} by ZMODUL06:20;
0. V in Lin ( the Basis of V \ {v}) by ZMODUL01:33;
then ((1. INT.Ring) * v) - ((pp * iu2) * v) = ((pp * iu2) * v) - ((pp * iu2) * v) by B5, B11, B6, B7, B9, B10, B12, ZMODUL01:134;
then ((1. INT.Ring) - (pp * iu2)) * v = ((pp * iu2) * v) - ((pp * iu2) * v) by ZMODUL01:9;
then (1. INT.Ring) - (pp * iu2) = 0 by A6, RLVECT_1:15;
then 1 / p is Integer by XCMPLX_1:89;
hence contradiction by INT_2:def 4, NAT_D:33; :: thesis: verum