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