let V be non trivial torsion-free finitely-generated Z_Module; :: thesis: not V is divisible
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
(Omega). V <> (0). V ;
then Lin I <> (0). V by A1, VECTSP_7:def 3;
then I <> {} the carrier of V by ZMODUL02:67;
then consider v being object such that
A3: v in I by XBOOLE_0:def 1;
reconsider v = v as Vector of V by A3;
A4: ( V is Submodule of V & I is linearly-independent & (Omega). V = Lin I ) by A1, ZMODUL01:32, VECTSP_7:def 3;
then A5: ( (Omega). V = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V ) by A3, ZMODUL06:24;
(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39
.= I by A3, XBOOLE_1:12, ZFMISC_1:31 ;
then B3: Lin I = (Lin (I \ {v})) + (Lin {v}) by ZMODUL02:72;
reconsider i2 = 2 as Element of INT.Ring by INT_1:def 2;
not v is divisible

proof

assume v is divisible ; :: thesis: contradiction
then consider u being Vector of V such that
C1: i2 * u = v ;
u in Lin I by A4;
then consider u1, u2 being Vector of V such that
C2: ( u1 in Lin (I \ {v}) & u2 in Lin {v} & u = u1 + u2 ) by B3, ZMODUL01:92;
consider iu2 being Element of INT.Ring such that
C3: u2 = iu2 * v by C2, ZMODUL06:19;
C4: u1 <> 0. V

proof

assume u1 = 0. V ; :: thesis: contradiction
then v = (i2 * iu2) * v by C1, C2, C3, VECTSP_1:def 16;
then ((i2 * iu2) * v) - v = 0. V by RLVECT_1:15;
then ((i2 * iu2) * v) - ((1. INT.Ring) * v) = 0. V by VECTSP_1:def 17;
then D1: ((i2 * iu2) - (1. INT.Ring)) * v = 0. V by ZMODUL01:9;
reconsider iiu2 = iu2 as Integer ;
(2 * iiu2) - 1 <> 0

proof

assume (2 * iiu2) - 1 = 0 ; :: thesis: contradiction
then 1 / 2 is Integer ;
hence contradiction by NAT_D:33; :: thesis: verum

end;

then v is torsion by D1;
hence contradiction by A5, ZMODUL06:def 3; :: thesis: verum

end;

v = (i2 * u1) + (i2 * u2) by C1, C2, VECTSP_1:def 14
.= (i2 * u1) + ((i2 * iu2) * v) by C3, VECTSP_1:def 16 ;
then v - ((i2 * iu2) * v) = (i2 * u1) + (((i2 * iu2) * v) - ((i2 * iu2) * v)) by RLVECT_1:28
.= (i2 * u1) + (0. V) by RLVECT_1:15
.= i2 * u1 ;
then ((1. INT.Ring) * v) - ((i2 * iu2) * v) = i2 * u1 by VECTSP_1:def 17;
then C5: ((1. INT.Ring) - (i2 * iu2)) * v = i2 * u1 by ZMODUL01:9;
i2 <> 0. INT.Ring ;
then C6: i2 * u1 <> 0. V by C4, ZMODUL01:def 7;
C7: i2 * u1 in Lin (I \ {v}) by C2, ZMODUL01:37;
((1. INT.Ring) - (i2 * iu2)) * v in Lin {v} by ZMODUL06:21;
hence contradiction by A5, C5, C6, C7, ZMODUL01:94, ZMODUL02:66; :: thesis: verum

end;

hence not V is divisible ; :: thesis: verum