let V be non trivial free Z_Module; :: thesis: for v being non zero Vector of V holds not v is divisible
let v be non zero Vector of V; :: thesis: not v is divisible
reconsider i2 = 2 as Element of INT.Ring by INT_1:def 2;
set I = the Basis of V;
A1: ( the Basis of V is linearly-independent & (Omega). V = Lin the Basis of V ) by VECTSP_7:def 3;
consider L being Linear_Combination of the Basis of V, u being Vector of V such that
A2: ( v = Sum L & u in the Basis of V & L . u <> 0 ) by LmND1;
assume v is divisible ; :: thesis: contradiction
then consider w being Vector of V such that
A5: (i2 * (L . u)) * w = v by A2;
w in Lin the Basis of V by A1;
then consider Lw being Linear_Combination of the Basis of V such that
A6: w = Sum Lw by ZMODUL02:64;
reconsider Luw = (i2 * (L . u)) * Lw as Linear_Combination of the Basis of V by ZMODUL02:31;
A8: Sum Luw = Sum L by A2, A5, A6, ZMODUL02:53;
( Carrier Luw c= the Basis of V & Carrier L c= the Basis of V ) by VECTSP_6:def 4;
then Luw = L by A8, VECTSP_7:def 3, ZMODUL03:3;
then L . u = (i2 * (L . u)) * (Lw . u) by VECTSP_6:def 9
.= (i2 * (Lw . u)) * (L . u) ;
then i2 * (Lw . u) = 1 by A2, XCMPLX_1:7;
hence contradiction by INT_1:9; :: thesis: verum