let V be Z_Module; :: thesis: ( V is Mult-cancelable implies ex I being Function of V,(Z_MQ_VectSp V) st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((EQRZM V),[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. (Z_MQ_VectSp V) ) )
assume AS: V is Mult-cancelable ; :: thesis: ex I being Function of V,(Z_MQ_VectSp V) st
( I is one-to-one & ( for v being Element of V holds I . v = Class ((EQRZM V),[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. (Z_MQ_VectSp V) )
then Z0: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by defZMQVSp;
X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1;
then X2: 1 in INT \ {0} by XBOOLE_0:def 5, X1;
set i1 = 1. INT.Ring;
defpred S₁[ Element of V, Element of (Z_MQ_VectSp V)] means $2 = Class ((EQRZM V),[$1,1]);
A2: for x being Element of V ex v being Element of (Z_MQ_VectSp V) st S₁[x,v]

proof

let x be Element of V; :: thesis: ex v being Element of (Z_MQ_VectSp V) st S₁[x,v]
X1: 1 in INT by INT_1:def 2;
not 1 in {0} by TARSKI:def 1;
then 1 in INT \ {0} by XBOOLE_0:def 5, X1;
then [x,1] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;
then reconsider z = Class ((EQRZM V),[x,1]) as Element of (Z_MQ_VectSp V) by Z0, EQREL_1:def 3;
z = Class ((EQRZM V),[x,1]) ;
hence ex z being Element of (Z_MQ_VectSp V) st S₁[x,z] ; :: thesis: verum

end;

consider F being Function of V,(Z_MQ_VectSp V) such that
X3: for x being Element of V holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
take F ; :: thesis: ( F is one-to-one & ( for v being Element of V holds F . v = Class ((EQRZM V),[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. (Z_MQ_VectSp V) )

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 ((EQRZM V),[x10,1]) by X3;
P2: [x10,1] in [: the carrier of V,(INT \ {0}):] by X2, ZFMISC_1:87;
Class ((EQRZM V),[x10,(1. INT.Ring)]) = Class ((EQRZM V),[x20,(1. INT.Ring)]) by A1, P1, X3;
then P3: [[x10,(1. INT.Ring)],[x20,(1. INT.Ring)]] in EQRZM V by P2, EQREL_1:35;
thus x1 = (1. INT.Ring) * x10 by VECTSP_1:def 17
.= (1. INT.Ring) * x20 by AS, P3, LMEQR001
.= 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 ((EQRZM V),[v,1]) by X3;
P2: F . w = Class ((EQRZM V),[w,1]) by X3;
P8: ((1. INT.Ring) * v) + ((1. INT.Ring) * w) = (1. INT.Ring) * (v + w) by VECTSP_1:def 14
.= v + w by VECTSP_1:def 17 ;
(F . v) + (F . w) = Class ((EQRZM V),[(((1. INT.Ring) * v) + ((1. INT.Ring) * w)),((1. INT.Ring) * (1. INT.Ring))]) by AS, P1, P2, Z0, DefaddCoset
.= 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 ((EQRZM V),[v,(1. INT.Ring)]) 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 ((EQRZM V),[(i * v),((1. INT.Ring) * (1. INT.Ring))]) by AS, P1, Z0, DeflmultCoset
.= F . (i * v) by X3 ;
hence F . (i * v) = x * (F . v) ; :: thesis: verum

end;

F . (0. V) = Class ((EQRZM V),[(0. V),1]) by X3
.= 0. (Z_MQ_VectSp V) by AS, Z0, defZero ;
hence ( F is one-to-one & ( for v being Element of V holds F . v = Class ((EQRZM V),[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. (Z_MQ_VectSp V) ) by S2, S3, S4, X3, FUNCT_2:19; :: thesis: verum