let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module
for s being FinSequence of V
for t being FinSequence of (Z_MQ_VectSp (V,p)) st len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = ZMtoMQV (V,p,si) ) ) holds
Sum t = ZMtoMQV (V,p,(Sum s))

let V be free Z_Module; :: thesis: for s being FinSequence of V
for t being FinSequence of (Z_MQ_VectSp (V,p)) st len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = ZMtoMQV (V,p,si) ) ) holds
Sum t = ZMtoMQV (V,p,(Sum s))

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

let t be FinSequence of (Z_MQ_VectSp (V,p)); :: thesis: ( len s = 0 & len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = ZMtoMQV (V,p,si) ) ) implies Sum t = ZMtoMQV (V,p,(Sum s)) )

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

let t be FinSequence of (Z_MQ_VectSp (V,p)); :: thesis: ( len s = k + 1 & len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = ZMtoMQV (V,p,si) ) ) implies Sum t = ZMtoMQV (V,p,(Sum s)) )

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

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

Seg k c= Seg (k + 1) by ;
then consider si being Vector of V such that
A19: ( si = s . i & t . i = ZMtoMQV (V,p,si) ) by A7, A11, A8, A18;
take si ; :: thesis: ( si = s1 . i & t1 . i = ZMtoMQV (V,p,si) )
thus si = s1 . i by ; :: thesis: t1 . i = ZMtoMQV (V,p,si)
thus t1 . i = ZMtoMQV (V,p,si) by ; :: thesis: verum
end;
A20: Sum t1 = ZMtoMQV (V,p,(Sum s1)) by A5, A16, A17;
A21: len s = (len s1) + 1 by ;
consider ssi being Vector of V such that
A22: ( ssi = s . (len s) & t . (len s) = ZMtoMQV (V,p,ssi) ) by ;
thus Sum t = (Sum t1) + vt by
.= ZMtoMQV (V,p,((Sum s1) + vs)) by A6, A20, A22, Th28
.= ZMtoMQV (V,p,(Sum s)) by ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A1, A4);
hence for s being FinSequence of V
for t being FinSequence of (Z_MQ_VectSp (V,p)) st len s = len t & ( for i being Element of NAT st i in dom s holds
ex si being Vector of V st
( si = s . i & t . i = ZMtoMQV (V,p,si) ) ) holds
Sum t = ZMtoMQV (V,p,(Sum s)) ; :: thesis: verum