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_{1}[ 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_{1}[x,v]

X3: for x being Element of V holds S_{1}[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) )

for i being Element of INT.Ring

for q being Element of F_Rat st i = q holds

F . (i * v) = q * (F . v)

.= 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

( 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

A2: for x being Element of V ex v being Element of (Z_MQ_VectSp V) st S

proof

consider F being Function of V,(Z_MQ_VectSp V) such that
let x be Element of V; :: thesis: ex v being Element of (Z_MQ_VectSp V) st S_{1}[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_{1}[x,z]
; :: thesis: verum

end;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

X3: for x being Element of V holds S

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

S3:
for v, w being Element of V holds F . (v + w) = (F . v) + (F . w)
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;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

proof

S4:
for v being Element of V
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;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

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

F . (0. V) =
Class ((EQRZM V),[(0. V),1])
by X3
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;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

.= 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