let V be Z_Module; :: thesis: for v being Vector of V st v is torsion & v <> 0. V holds
not Lin {v} is divisible
let v be Vector of V; :: thesis: ( v is torsion & v <> 0. V implies not Lin {v} is divisible )
assume A1: ( v is torsion & v <> 0. V ) ; :: thesis: not Lin {v} is divisible
consider i being Element of INT.Ring such that
A2: ( i <> 0 & i * v = 0. V ) by A1;
assume A3: Lin {v} is divisible ; :: thesis: contradiction
v in Lin {v} by ZMODUL06:20;
then reconsider vv = v as Vector of (Lin {v}) ;
vv is divisible by A3;
then consider uu being Vector of (Lin {v}) such that
A4: i * uu = vv by A2;
reconsider u = uu as Vector of V by ZMODUL01:25;
u in Lin {v} ;
then consider b being Element of INT.Ring such that
A5: u = b * v by ZMODUL06:19;
vv = i * (b * v) by A4, A5, ZMODUL01:29
.= (i * b) * v by VECTSP_1:def 16
.= b * (i * v) by VECTSP_1:def 16
.= 0. V by A2, ZMODUL01:1 ;
hence contradiction by A1; :: thesis: verum