let V be Z_Module; :: thesis: ( V is Mult-cancelable implies ex I being Function of V,() st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
I . (i * v) = q * (I . v) ) & I . (0. V) = 0. () ) )

assume AS: V is Mult-cancelable ; :: thesis: ex I being Function of V,() st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
I . (i * v) = q * (I . v) ) & I . (0. V) = 0. () )

then Z0: Z_MQ_VectSp V = ModuleStr(# (Class ()),(),(),() #) by defZMQVSp;
X1: 1 in INT by INT_1:def 2;
not 1 in by TARSKI:def 1;
then X2: 1 in INT \ by ;
set i1 = 1. INT.Ring;
defpred S1[ Element of V, Element of ()] means \$2 = Class ((),[\$1,1]);
A2: for x being Element of V ex v being Element of () st S1[x,v]
proof
let x be Element of V; :: thesis: ex v being Element of () st S1[x,v]
X1: 1 in INT by INT_1:def 2;
not 1 in by TARSKI:def 1;
then 1 in INT \ by ;
then [x,1] in [: the carrier of V,():] by ZFMISC_1:87;
then reconsider z = Class ((),[x,1]) as Element of () by ;
z = Class ((),[x,1]) ;
hence ex z being Element of () st S1[x,z] ; :: thesis: verum
end;
consider F being Function of V,() such that
X3: for x being Element of V holds S1[x,F . x] from take F ; :: thesis: ( F is one-to-one & ( for v being Element of V holds F . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds F . (v + w) = (F . v) + (F . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v) ) & F . (0. V) = 0. () )

S2: now :: thesis: for x1, x2 being object st x1 in the carrier of V & x2 in the carrier of V & F . x1 = F . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in the carrier of V & x2 in the carrier of V & F . x1 = F . x2 implies x1 = x2 )
assume A1: ( x1 in the carrier of V & x2 in the carrier of V & F . x1 = F . x2 ) ; :: thesis: x1 = x2
then reconsider x10 = x1, x20 = x2 as Element of V ;
P1: F . x1 = Class ((),[x10,1]) by X3;
P2: [x10,1] in [: the carrier of V,():] by ;
Class ((),[x10,()]) = Class ((),[x20,()]) by A1, P1, X3;
then P3: [[x10,()],[x20,()]] in EQRZM V by ;
thus x1 = () * x10 by VECTSP_1:def 17
.= () * x20 by
.= x2 by VECTSP_1:def 17 ; :: thesis: verum
end;
S3: for v, w being Element of V holds F . (v + w) = (F . v) + (F . w)
proof
let v, w be Element of V; :: thesis: F . (v + w) = (F . v) + (F . w)
P1: F . v = Class ((),[v,1]) by X3;
P2: F . w = Class ((),[w,1]) by X3;
P8: (() * v) + (() * w) = () * (v + w) by VECTSP_1:def 14
.= v + w by VECTSP_1:def 17 ;
(F . v) + (F . w) = Class ((),[((() * v) + (() * w)),(() * ())]) by
.= F . (v + w) by P8, X3 ;
hence F . (v + w) = (F . v) + (F . w) ; :: thesis: verum
end;
S4: for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v)
proof
let v be Element of V; :: thesis: for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v)

let i be Element of INT.Ring; :: thesis: for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v)

let x be Element of F_Rat; :: thesis: ( i = x implies F . (i * v) = x * (F . v) )
assume AS0: i = x ; :: thesis: F . (i * v) = x * (F . v)
P1: F . v = Class ((),[v,()]) by X3;
reconsider ii = i, ii1 = 1. INT.Ring as Integer ;
( 1. INT.Ring <> 0. INT.Ring & x = ii / ii1 ) by AS0;
then x * (F . v) = Class ((),[(i * v),(() * ())]) by
.= F . (i * v) by X3 ;
hence F . (i * v) = x * (F . v) ; :: thesis: verum
end;
F . (0. V) = Class ((),[(0. V),1]) by X3
.= 0. () by ;
hence ( F is one-to-one & ( for v being Element of V holds F . v = Class ((),[v,1]) ) & ( for v, w being Element of V holds F . (v + w) = (F . v) + (F . w) ) & ( for v being Element of V
for i being Element of INT.Ring
for q being Element of F_Rat st i = q holds
F . (i * v) = q * (F . v) ) & F . (0. V) = 0. () ) by ; :: thesis: verum