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;

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 )

hence
ZMtoMQV (V,p,(Sum l)) in Lin IQ
by AS, P1, ZMODUL03:33; :: thesis: verumex 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;( 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