let p be prime Element of INT.Ring; :: thesis:
let V be free Z_Module; :: thesis:
let I be Basis of V; :: thesis:
let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis:
let l be Linear_Combination of I; :: thesis:
assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis:
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:

let i be Element of NAT ; :: thesis:
assume i in dom (l (#) G) ; :: thesis:
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 A3, ZMODUL02:13;
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 A3, A2, FUNCT_1:3;
Carrier l c= I by VECTSP_6:def 4;
then t in IQ by A1, A6;
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 A5, A4; :: thesis:

end;

hence ZMtoMQV (V,p,(Sum l)) in Lin IQ by A1, A2, Th33; :: thesis: