let V be non trivial torsion-free Z_Module; :: thesis:
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]

let i be Element of INT.Ring; :: thesis:
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:
thus S₁[i,w] ; :: thesis:

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

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

let x1, x2 be object ; :: thesis:
assume B1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
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:

end;

end;