let V be non trivial torsion-free Z_Module; :: thesis: V is infinite
set v = the non zero Vector of V;
defpred S₁[ object , object ] means for i being Element of INT.Ring st i = c₁ holds
c₂ = i * the non zero Vector of V;
A1: for i being Element of INT.Ring ex w being Element of (Lin { the non zero Vector of V}) st S₁[i,w]

proof

let i be Element of INT.Ring; :: thesis: ex w being Element of (Lin { the non zero Vector of V}) st S₁[i,w]
set w = i * the non zero Vector of V;
i * the non zero Vector of V in Lin { the non zero Vector of V} by ZMODUL06:21;
then reconsider w = i * the non zero Vector of V as Element of (Lin { the non zero Vector of V}) ;
take w ; :: thesis: S₁[i,w]
thus S₁[i,w] ; :: thesis: verum

end;

ex f being Function of INT.Ring,(Lin { the non zero Vector of V}) st
for i being Element of INT.Ring holds S₁[i,f . i] from FUNCT_2:sch 3(A1);
then consider f being Function of INT.Ring,(Lin { the non zero Vector of V}) such that
A2: for i being Element of INT.Ring holds S₁[i,f . i] ;
A3: ( dom f = INT & rng f c= the carrier of (Lin { the non zero Vector of V}) ) by FUNCT_2:def 1;
f is one-to-one

proof

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume B1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
reconsider xx1 = x1, xx2 = x2 as Element of INT.Ring by B1;
f . x1 = xx1 * the non zero Vector of V by A2;
then xx1 * the non zero Vector of V = xx2 * the non zero Vector of V by A2, B1;
then (xx1 * the non zero Vector of V) - (xx2 * the non zero Vector of V) = 0. V by RLVECT_1:15;
then (xx1 - xx2) * the non zero Vector of V = 0. V by ZMODUL01:9;
then xx1 - xx2 = 0. INT.Ring by ZMODUL01:def 7;
hence x1 = x2 ; :: thesis: verum

end;

hence f is one-to-one by FUNCT_1:def 4; :: thesis: verum

end;

then A4: card INT c= card (Lin { the non zero Vector of V}) by A3, CARD_1:10;
the carrier of (Lin { the non zero Vector of V}) is Subset of the carrier of V by VECTSP_4:def 2;
hence V is infinite by A4; :: thesis: verum