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))

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 )
;

end;

suppose A3:
I is empty
; :: thesis: Sum lq = ZMtoMQV (V,p,(Sum l))

IQ = {}

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;proof

then
IQ = {} the carrier of (Z_MQ_VectSp (V,p))
;
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 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

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

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 )

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;

end;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

then
rng FGq = Carrier l
by TARSKI:2;
let x be object ; :: thesis: ( x in rng FGq iff x in Carrier l )

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;hereby :: thesis: ( x in Carrier l implies x in rng FGq )

assume A20:
x in Carrier l
; :: thesis: x in rng FGqassume
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;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

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

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) )

hence
Sum lq = ZMtoMQV (V,p,(Sum l))
by A9, A27, A29, A30, Th29; :: thesis: verumex 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;( 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