let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module
for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p))
for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ZMtoMQV (V,p,(Sum l)) in Lin IQ

let V be free Z_Module; :: thesis: for I being Basis of V
for IQ being Subset of (Z_MQ_VectSp (V,p))
for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ZMtoMQV (V,p,(Sum l)) in Lin IQ

let I be Basis of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p))
for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ZMtoMQV (V,p,(Sum l)) in Lin IQ

let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis: for l being Linear_Combination of I st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ZMtoMQV (V,p,(Sum l)) in Lin IQ

let l be Linear_Combination of I; :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies ZMtoMQV (V,p,(Sum l)) in Lin IQ )
assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: ZMtoMQV (V,p,(Sum l)) in Lin IQ
consider G being FinSequence of V such that
A2: ( G is one-to-one & rng G = Carrier l & Sum l = Sum (l (#) G) ) by VECTSP_6:def 6;
now :: thesis: for i being Element of NAT st i in dom (l (#) G) holds
ex si being Vector of V st
( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ )
let i be Element of NAT ; :: thesis: ( i in dom (l (#) G) implies ex si being Vector of V st
( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ ) )

assume i in dom (l (#) G) ; :: thesis: ex si being Vector of V st
( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ )

then i in Seg (len (l (#) G)) by FINSEQ_1:def 3;
then i in Seg (len G) by VECTSP_6:def 5;
then A3: i in dom G by FINSEQ_1:def 3;
then G . i in rng G by FUNCT_1:3;
then reconsider v = G . i as Element of V ;
A4: (l (#) G) . i = (l . v) * v by ;
reconsider b = (l . v) mod p as Element of (GF p) by Lm3;
reconsider a = (l . v) mod p as Element of INT.Ring ;
reconsider k = l . v as Element of INT.Ring ;
reconsider t = ZMtoMQV (V,p,v) as Element of (Z_MQ_VectSp (V,p)) ;
A5: b * t = ZMtoMQV (V,p,(a * v)) by Th30
.= ZMtoMQV (V,p,(k * v)) by Lm4 ;
A6: v in Carrier l by ;
Carrier l c= I by VECTSP_6:def 4;
then t in IQ by A1, A6;
then b * t in Lin IQ by ;
hence ex si being Vector of V st
( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ ) by A5, A4; :: thesis: verum
end;
hence ZMtoMQV (V,p,(Sum l)) in Lin IQ by A1, A2, Th33; :: thesis: verum