let p be Prime; :: 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, ZMODUL02:def 10;
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, ZMODUL01:def 13;
take v ; :: thesis: vq = ZMtoMQV (V,p,v)
thus vq = ZMtoMQV (V,p,v) by A3; :: thesis: verum