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 A6, Th27; :: 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 Th25, A1;
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 A10, A9, A8, RELAT_1:27, VECTSP_6:def 4;
A13: rng (F * Gq) c= the carrier of V ;
F * Gq is FinSequence by A8, A9, FINSEQ_1:16, VECTSP_6:def 4;
then reconsider FGq = F * Gq as FinSequence of V by A13, FINSEQ_1:def 4;
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: x in Carrier l
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 A14, FUNCT_1:12;
A16: ( z in dom Gq & Gq . z in dom F ) by A14, FUNCT_1:11;
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 A8, A17;
consider w being Element of (Z_MQ_VectSp (V,p)) such that
A19: ( Gq . z = w & lq . w <> 0. (GF p) ) by A9, A16, FUNCT_1:3, VECTSP_6:1;
l . u <> 0. (GF p) by A2, A17, A19;
then l . u <> 0 by EC_PF_1:11;
hence x in Carrier l by A15, A18; :: 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 A20, ZMODUL02:8;
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 A11, A9, A24, A8, A23, FUNCT_1:11;
then FGq . z = u by A25, FUNCT_1:12;
hence x in rng FGq by A26, FUNCT_1:def 3; :: thesis: verum

end;

then rng FGq = Carrier l by TARSKI:2;
then A27: Sum l = Sum (l (#) FGq) by A9, A8, VECTSP_6:def 6;
A28: len (l (#) FGq) = len FGq by VECTSP_6:def 5;
then A29: len (l (#) FGq) = len Gq by A12, FINSEQ_1:def 3;
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 A28, FINSEQ_1:def 3;
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 A32, ZMODUL02:13;
i in Seg (len Gq) by A29, A31, FINSEQ_1:def 3;
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 A9, A11;
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 A1, A36;
F . (Gq . i) = u by A8, A37;
then A38: v = u by A32, FUNCT_1:12;
(lq (#) Gq) . i = (lq . w) * w by A34, VECTSP_6:8
.= 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;