let p be prime Element of INT.Ring; :: thesis: for V being Z_Module

for ZQ being VectSp of GF p

for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

let V be Z_Module; :: thesis: for ZQ being VectSp of GF p

for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

let ZQ be VectSp of GF p; :: thesis: for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

let vq be Vector of ZQ; :: thesis: ( ZQ = Z_MQ_VectSp (V,p) implies ex v being Vector of V st vq = ZMtoMQV (V,p,v) )

assume A1: ZQ = Z_MQ_VectSp (V,p) ; :: thesis: ex v being Vector of V st vq = ZMtoMQV (V,p,v)

vq is Element of CosetSet (V,(p (*) V)) by A1, VECTSP10:def 6;

then vq in { A where A is Coset of p (*) V : verum } ;

then consider vqq being Coset of p (*) V such that

A2: vqq = vq ;

consider v being Vector of V such that

A3: vq = v + (p (*) V) by A2, VECTSP_4:def 6;

take v ; :: thesis: vq = ZMtoMQV (V,p,v)

thus vq = ZMtoMQV (V,p,v) by A3; :: thesis: verum

for ZQ being VectSp of GF p

for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

let V be Z_Module; :: thesis: for ZQ being VectSp of GF p

for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

let ZQ be VectSp of GF p; :: thesis: for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds

ex v being Vector of V st vq = ZMtoMQV (V,p,v)

let vq be Vector of ZQ; :: thesis: ( ZQ = Z_MQ_VectSp (V,p) implies ex v being Vector of V st vq = ZMtoMQV (V,p,v) )

assume A1: ZQ = Z_MQ_VectSp (V,p) ; :: thesis: ex v being Vector of V st vq = ZMtoMQV (V,p,v)

vq is Element of CosetSet (V,(p (*) V)) by A1, VECTSP10:def 6;

then vq in { A where A is Coset of p (*) V : verum } ;

then consider vqq being Coset of p (*) V such that

A2: vqq = vq ;

consider v being Vector of V such that

A3: vq = v + (p (*) V) by A2, VECTSP_4:def 6;

take v ; :: thesis: vq = ZMtoMQV (V,p,v)

thus vq = ZMtoMQV (V,p,v) by A3; :: thesis: verum