let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module
for I being Subset 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 Subset 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 Subset 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 AS: 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
P1: ( 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 Y3: 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 ;
Y5: (l (#) G) . i = (l . v) * v by Y3, ZMODUL02:13;
reconsider b = (l . v) mod p as Element of (GF p) by EC_PF_1:14;
reconsider a = (l . v) mod p as Element of INT.Ring ;
reconsider k = l . v as Element of INT.Ring ;
reconsider si = (l . v) * v as Element of V ;
reconsider t = ZMtoMQV (V,p,v) as Element of (Z_MQ_VectSp (V,p)) ;
Y7: b * t = ZMtoMQV (V,p,(a * v)) by ZMODUL03:30
.= ZMtoMQV (V,p,(k * v)) by LMX2 ;
H1: v in Carrier l by Y3, P1, FUNCT_1:3;
Carrier l c= I by VECTSP_6:def 4;
then t in IQ by AS, H1;
then b * t in Lin IQ by VECTSP_4:21, VECTSP_7:8;
hence ex si being Vector of V st
( si = (l (#) G) . i & ZMtoMQV (V,p,si) in Lin IQ ) by Y7, Y5; :: thesis: verum

end;

hence ZMtoMQV (V,p,(Sum l)) in Lin IQ by AS, P1, ZMODUL03:33; :: thesis: verum