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 S₁[ 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: S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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 A5, FINSEQ_1:def 3;
A8: len s1 = k by A5, FINSEQ_1:59, NAT_1:11;
A9: dom s1 = Seg (len s1) by FINSEQ_1:def 3
.= Seg k by A5, FINSEQ_1:59, NAT_1:11 ;
then A10: s1 = s | (dom s1) by FINSEQ_1:def 16;
s . (len s) in rng s by A5, A7, FINSEQ_1:4, FUNCT_1:3;
then reconsider vs = s . (len s) as Element of V ;
A11: len s1 = k by A5, FINSEQ_1:59, NAT_1:11;
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 FINSEQ_1:5, NAT_1:11;
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 A10, A13, A14, FUNCT_1:49; :: 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 A5, A6, A7, FINSEQ_1:4;
ZMtoMQV (V,p,(Sum s)) = ZMtoMQV (V,p,((Sum s1) + vs)) by A5, A10, A8, RLVECT_1:38
.= (ZMtoMQV (V,p,(Sum s1))) + (ZMtoMQV (V,p,vs)) by Th28 ;
hence ZMtoMQV (V,p,(Sum s)) in Lin IQ by A15, A16, VECTSP_4:20; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A17: for k being Nat holds S₁[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 A17, A18; :: 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