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

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

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

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

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

let lq be Linear_Combination of IQ; :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) implies Sum lq = ZMtoMQV (V,p,(Sum l)) )

assume A1: IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: ( ex v being Vector of V st
( v in I & not l . v = lq . (ZMtoMQV (V,p,v)) ) or Sum lq = ZMtoMQV (V,p,(Sum l)) )

assume A2: for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ; :: thesis: Sum lq = ZMtoMQV (V,p,(Sum l))
per cases ( I is empty or not I is empty ) ;
suppose A3: I is empty ; :: thesis: Sum lq = ZMtoMQV (V,p,(Sum l))
IQ = {}
proof
assume IQ <> {} ; :: thesis: contradiction
then consider v0 being object such that
A4: v0 in IQ by XBOOLE_0:def 1;
consider u being Vector of V such that
A5: ( v0 = ZMtoMQV (V,p,u) & u in I ) by A4, A1;
thus contradiction by A5, A3; :: thesis: verum
end;
then IQ = {} the carrier of (Z_MQ_VectSp (V,p)) ;
then lq = ZeroLC (Z_MQ_VectSp (V,p)) by VECTSP_6:6;
then A6: Sum lq = 0. (Z_MQ_VectSp (V,p)) by VECTSP_6:15;
I = {} the carrier of V by A3;
then l = ZeroLC V by ZMODUL02:12;
then Sum l = 0. V by ZMODUL02:19;
hence Sum lq = ZMtoMQV (V,p,(Sum l)) by ; :: thesis: verum
end;
suppose not I is empty ; :: thesis: Sum lq = ZMtoMQV (V,p,(Sum l))
then consider v0 being object such that
A7: v0 in I by XBOOLE_0:def 1;
reconsider v0 = v0 as Vector of V by A7;
ZMtoMQV (V,p,v0) in IQ by A7, A1;
then reconsider X = IQ as non empty Subset of (Z_MQ_VectSp (V,p)) ;
consider F being Function of X, the carrier of V such that
A8: ( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I ) by ;
consider Gq being FinSequence of (Z_MQ_VectSp (V,p)) such that
A9: ( Gq is one-to-one & rng Gq = Carrier lq & Sum lq = Sum (lq (#) Gq) ) by VECTSP_6:def 6;
set n = len Gq;
A10: dom Gq = Seg (len Gq) by FINSEQ_1:def 3;
A11: Carrier lq c= X by VECTSP_6:def 4;
A12: dom (F * Gq) = Seg (len Gq) by ;
A13: rng (F * Gq) c= the carrier of V ;
F * Gq is FinSequence by ;
then reconsider FGq = F * Gq as FinSequence of V by ;
for x being object holds
( x in rng FGq iff x in Carrier l )
proof
let x be object ; :: thesis: ( x in rng FGq iff x in Carrier l )
hereby :: thesis: ( x in Carrier l implies x in rng FGq )
assume x in rng FGq ; :: thesis:
then consider z being object such that
A14: ( z in dom FGq & x = FGq . z ) by FUNCT_1:def 3;
A15: x = F . (Gq . z) by ;
A16: ( z in dom Gq & Gq . z in dom F ) by ;
then consider u being Vector of V such that
A17: ( Gq . z = ZMtoMQV (V,p,u) & u in I ) by A1, A8;
A18: F . (Gq . z) = u by ;
consider w being Element of (Z_MQ_VectSp (V,p)) such that
A19: ( Gq . z = w & lq . w <> 0. (GF p) ) by ;
l . u <> 0. (GF p) by A2, A17, A19;
then l . u <> 0 by EC_PF_1:11;
hence x in Carrier l by ; :: thesis: verum
end;
assume A20: x in Carrier l ; :: thesis: x in rng FGq
then reconsider u = x as Vector of V ;
A21: l . u <> 0 by ;
A22: Carrier l c= I by VECTSP_6:def 4;
then lq . (ZMtoMQV (V,p,u)) <> 0 by A2, A21, A20;
then lq . (ZMtoMQV (V,p,u)) <> 0. (GF p) by EC_PF_1:11;
then A23: ZMtoMQV (V,p,u) in rng Gq by A9;
then consider z being object such that
A24: ( z in dom Gq & ZMtoMQV (V,p,u) = Gq . z ) by FUNCT_1:def 3;
A25: F . (Gq . z) = u by A20, A22, A24, A8;
A26: z in dom FGq by ;
then FGq . z = u by ;
hence x in rng FGq by ; :: thesis: verum
end;
then rng FGq = Carrier l by TARSKI:2;
then A27: Sum l = Sum (l (#) FGq) by ;
A28: len (l (#) FGq) = len FGq by VECTSP_6:def 5;
then A29: len (l (#) FGq) = len Gq by ;
A30: len (lq (#) Gq) = len Gq by VECTSP_6:def 5;
now :: thesis: for i being Element of NAT st i in dom (l (#) FGq) holds
ex si being Vector of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = ZMtoMQV (V,p,si) )
let i be Element of NAT ; :: thesis: ( i in dom (l (#) FGq) implies ex si being Vector of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = ZMtoMQV (V,p,si) ) )

assume A31: i in dom (l (#) FGq) ; :: thesis: ex si being Vector of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = ZMtoMQV (V,p,si) )

then i in Seg (len FGq) by ;
then A32: i in dom FGq by FINSEQ_1:def 3;
then FGq . i in rng FGq by FUNCT_1:3;
then reconsider v = FGq . i as Element of V ;
A33: (l (#) FGq) . i = (l . v) * v by ;
i in Seg (len Gq) by ;
then A34: i in dom Gq by FINSEQ_1:def 3;
then A35: Gq . i in rng Gq by FUNCT_1:3;
then A36: Gq . i in X by ;
reconsider w = Gq . i as Element of (Z_MQ_VectSp (V,p)) by A35;
consider u being Vector of V such that
A37: ( Gq . i = ZMtoMQV (V,p,u) & u in I ) by ;
F . (Gq . i) = u by ;
then A38: v = u by ;
(lq (#) Gq) . i = (lq . w) * w by
.= ZMtoMQV (V,p,((l . v) * v)) by A2, A37, A38, Th30 ;
hence ex si being Vector of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = ZMtoMQV (V,p,si) ) by A33; :: thesis: verum
end;
hence Sum lq = ZMtoMQV (V,p,(Sum l)) by A9, A27, A29, A30, Th29; :: thesis: verum
end;
end;