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)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) 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)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp (V,p)) st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ

let IQ be Subset of (Z_MQ_VectSp (V,p)); :: thesis: ( IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ )

assume IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ

defpred S1[ Nat] means for s being FinSequence of V st len s = \$1 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ;
A1: S1[ 0 ]
proof
let s be FinSequence of V; :: thesis: ( len s = 0 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) implies ZMtoMQV (V,p,(Sum s)) in Lin IQ )

assume that
A2: len s = 0 and
for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ; :: thesis: ZMtoMQV (V,p,(Sum s)) in Lin IQ
s = <*> the carrier of V by A2;
then Sum s = 0. V by RLVECT_1:43;
then ZMtoMQV (V,p,(Sum s)) = 0. (Z_MQ_VectSp (V,p)) by Th27;
hence ZMtoMQV (V,p,(Sum s)) in Lin IQ by VECTSP_4:17; :: thesis: verum
end;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for s being FinSequence of V st len s = k + 1 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ
let s be FinSequence of V; :: thesis: ( len s = k + 1 & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) implies ZMtoMQV (V,p,(Sum s)) in Lin IQ )

assume that
A5: len s = k + 1 and
A6: for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ; :: thesis: ZMtoMQV (V,p,(Sum s)) in Lin IQ
reconsider s1 = s | k as FinSequence of V ;
A7: dom s = Seg (k + 1) by ;
A8: len s1 = k by ;
A9: dom s1 = Seg (len s1) by FINSEQ_1:def 3
.= Seg k by ;
then A10: s1 = s | (dom s1) by FINSEQ_1:def 15;
s . (len s) in rng s by ;
then reconsider vs = s . (len s) as Element of V ;
A11: len s1 = k by ;
A12: for i being Element of NAT st i in dom s1 holds
ex si being Vector of V st
( si = s1 . i & ZMtoMQV (V,p,si) in Lin IQ )
proof
let i be Element of NAT ; :: thesis: ( i in dom s1 implies ex si being Vector of V st
( si = s1 . i & ZMtoMQV (V,p,si) in Lin IQ ) )

assume A13: i in dom s1 ; :: thesis: ex si being Vector of V st
( si = s1 . i & ZMtoMQV (V,p,si) in Lin IQ )

Seg k c= Seg (k + 1) by ;
then consider si being Vector of V such that
A14: ( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) by A6, A9, A7, A13;
take si ; :: thesis: ( si = s1 . i & ZMtoMQV (V,p,si) in Lin IQ )
thus si = s1 . i by ; :: thesis: ZMtoMQV (V,p,si) in Lin IQ
thus ZMtoMQV (V,p,si) in Lin IQ by A14; :: thesis: verum
end;
A15: ZMtoMQV (V,p,(Sum s1)) in Lin IQ by A4, A11, A12;
consider ssi being Vector of V such that
A16: ( ssi = s . (len s) & ZMtoMQV (V,p,ssi) in Lin IQ ) by ;
ZMtoMQV (V,p,(Sum s)) = ZMtoMQV (V,p,((Sum s1) + vs)) by
.= (ZMtoMQV (V,p,(Sum s1))) + (ZMtoMQV (V,p,vs)) by Th28 ;
hence ZMtoMQV (V,p,(Sum s)) in Lin IQ by ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A17: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A3);
now :: thesis: for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ
let s be FinSequence of V; :: thesis: ( ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) implies ZMtoMQV (V,p,(Sum s)) in Lin IQ )

assume A18: for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ; :: thesis: ZMtoMQV (V,p,(Sum s)) in Lin IQ
len s = len s ;
hence ZMtoMQV (V,p,(Sum s)) in Lin IQ by ; :: thesis: verum
end;
hence for s being FinSequence of V st ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & ZMtoMQV (V,p,si) in Lin IQ ) ) holds
ZMtoMQV (V,p,(Sum s)) in Lin IQ ; :: thesis: verum