let V be Z_Module; :: thesis: ( V is Mult-cancelable implies for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s) )

assume AS: V is Mult-cancelable ; :: thesis: for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

defpred S_{1}[ Nat] means for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s);

A1: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A1, A4);

hence for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s) ; :: thesis: verum

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s) )

assume AS: V is Mult-cancelable ; :: thesis: for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

defpred S

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s);

A1: S

proof

A4:
for k being Nat st S
let s be FinSequence of V; :: thesis: for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

let t be FinSequence of (Z_MQ_VectSp V); :: 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 = (MorphsZQ V) . si ) ) implies Sum t = (MorphsZQ V) . (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 = (MorphsZQ V) . si ) ; :: thesis: Sum t = (MorphsZQ V) . (Sum s)

s = <*> the carrier of V by A2;

then Sum s = 0. V by RLVECT_1:43;

then A3: (MorphsZQ V) . (Sum s) = 0. (Z_MQ_VectSp V) by defMorph, AS;

t = <*> the carrier of (Z_MQ_VectSp V) by A2;

hence Sum t = (MorphsZQ V) . (Sum s) by A3, RLVECT_1:43; :: thesis: verum

end;ex si being Vector of V st

( si = s . i & t . i = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

let t be FinSequence of (Z_MQ_VectSp V); :: 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 = (MorphsZQ V) . si ) ) implies Sum t = (MorphsZQ V) . (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 = (MorphsZQ V) . si ) ; :: thesis: Sum t = (MorphsZQ V) . (Sum s)

s = <*> the carrier of V by A2;

then Sum s = 0. V by RLVECT_1:43;

then A3: (MorphsZQ V) . (Sum s) = 0. (Z_MQ_VectSp V) by defMorph, AS;

t = <*> the carrier of (Z_MQ_VectSp V) by A2;

hence Sum t = (MorphsZQ V) . (Sum s) by A3, RLVECT_1:43; :: thesis: verum

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A5: S

now :: thesis: for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

hence
Sfor t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

let s be FinSequence of V; :: thesis: for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

let t be FinSequence of (Z_MQ_VectSp V); :: 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 = (MorphsZQ V) . si ) ) implies Sum t = (MorphsZQ V) . (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 = (MorphsZQ V) . si ) ; :: thesis: Sum t = (MorphsZQ V) . (Sum s)

reconsider s1 = s | k as FinSequence of V ;

A8: dom s = Seg (k + 1) by A6, FINSEQ_1:def 3;

A9: dom t = Seg (k + 1) by A6, FINSEQ_1:def 3;

A10: len s1 = k by A6, FINSEQ_1:59, NAT_1:11;

A11: dom s1 = Seg (len s1) by FINSEQ_1:def 3

.= Seg k by A6, FINSEQ_1:59, NAT_1:11 ;

then A12: s1 = s | (dom s1) by FINSEQ_1:def 15;

reconsider t1 = t | k as FinSequence of (Z_MQ_VectSp V) ;

A13: dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg k by A6, FINSEQ_1:59, NAT_1:11 ;

then A14: t1 = t | (dom t1) by FINSEQ_1:def 15;

k in NAT by ORDINAL1:def 12;

then A15: len t1 = k by A13, FINSEQ_1:def 3;

s . (len s) in rng s by A6, A8, FINSEQ_1:4, FUNCT_1:3;

then reconsider vs = s . (len s) as Element of V ;

t . (len t) in rng t by A6, A9, FINSEQ_1:4, FUNCT_1:3;

then reconsider vt = t . (len t) as Element of (Z_MQ_VectSp V) ;

A16: ( len s1 = k & len s1 = len t1 ) by A10, A13, FINSEQ_1:def 3;

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 = (MorphsZQ V) . si )

A21: len s = (len s1) + 1 by A6, FINSEQ_1:59, NAT_1:11;

consider ssi being Vector of V such that

A22: ( ssi = s . (len s) & t . (len s) = (MorphsZQ V) . ssi ) by A6, A7, A8, FINSEQ_1:4;

thus Sum t = (Sum t1) + vt by A6, A14, A15, RLVECT_1:38

.= (MorphsZQ V) . ((Sum s1) + vs) by AS, A6, A20, A22, defMorph

.= (MorphsZQ V) . (Sum s) by A12, A21, RLVECT_1:38 ; :: thesis: verum

end;ex si being Vector of V st

( si = s . i & t . i = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s)

let t be FinSequence of (Z_MQ_VectSp V); :: 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 = (MorphsZQ V) . si ) ) implies Sum t = (MorphsZQ V) . (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 = (MorphsZQ V) . si ) ; :: thesis: Sum t = (MorphsZQ V) . (Sum s)

reconsider s1 = s | k as FinSequence of V ;

A8: dom s = Seg (k + 1) by A6, FINSEQ_1:def 3;

A9: dom t = Seg (k + 1) by A6, FINSEQ_1:def 3;

A10: len s1 = k by A6, FINSEQ_1:59, NAT_1:11;

A11: dom s1 = Seg (len s1) by FINSEQ_1:def 3

.= Seg k by A6, FINSEQ_1:59, NAT_1:11 ;

then A12: s1 = s | (dom s1) by FINSEQ_1:def 15;

reconsider t1 = t | k as FinSequence of (Z_MQ_VectSp V) ;

A13: dom t1 = Seg (len t1) by FINSEQ_1:def 3

.= Seg k by A6, FINSEQ_1:59, NAT_1:11 ;

then A14: t1 = t | (dom t1) by FINSEQ_1:def 15;

k in NAT by ORDINAL1:def 12;

then A15: len t1 = k by A13, FINSEQ_1:def 3;

s . (len s) in rng s by A6, A8, FINSEQ_1:4, FUNCT_1:3;

then reconsider vs = s . (len s) as Element of V ;

t . (len t) in rng t by A6, A9, FINSEQ_1:4, FUNCT_1:3;

then reconsider vt = t . (len t) as Element of (Z_MQ_VectSp V) ;

A16: ( len s1 = k & len s1 = len t1 ) by A10, A13, FINSEQ_1:def 3;

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 = (MorphsZQ V) . si )

proof

A20:
Sum t1 = (MorphsZQ V) . (Sum s1)
by A5, A16, A17;
let i be Element of NAT ; :: thesis: ( i in dom s1 implies ex si being Vector of V st

( si = s1 . i & t1 . i = (MorphsZQ V) . si ) )

assume A18: i in dom s1 ; :: thesis: ex si being Vector of V st

( si = s1 . i & t1 . i = (MorphsZQ V) . si )

Seg k c= Seg (k + 1) by FINSEQ_1:5, NAT_1:11;

then consider si being Vector of V such that

A19: ( si = s . i & t . i = (MorphsZQ V) . si ) by A7, A11, A8, A18;

take si ; :: thesis: ( si = s1 . i & t1 . i = (MorphsZQ V) . si )

thus si = s1 . i by A12, A18, A19, FUNCT_1:49; :: thesis: t1 . i = (MorphsZQ V) . si

thus t1 . i = (MorphsZQ V) . si by A14, A11, A13, A18, A19, FUNCT_1:49; :: thesis: verum

end;( si = s1 . i & t1 . i = (MorphsZQ V) . si ) )

assume A18: i in dom s1 ; :: thesis: ex si being Vector of V st

( si = s1 . i & t1 . i = (MorphsZQ V) . si )

Seg k c= Seg (k + 1) by FINSEQ_1:5, NAT_1:11;

then consider si being Vector of V such that

A19: ( si = s . i & t . i = (MorphsZQ V) . si ) by A7, A11, A8, A18;

take si ; :: thesis: ( si = s1 . i & t1 . i = (MorphsZQ V) . si )

thus si = s1 . i by A12, A18, A19, FUNCT_1:49; :: thesis: t1 . i = (MorphsZQ V) . si

thus t1 . i = (MorphsZQ V) . si by A14, A11, A13, A18, A19, FUNCT_1:49; :: thesis: verum

A21: len s = (len s1) + 1 by A6, FINSEQ_1:59, NAT_1:11;

consider ssi being Vector of V such that

A22: ( ssi = s . (len s) & t . (len s) = (MorphsZQ V) . ssi ) by A6, A7, A8, FINSEQ_1:4;

thus Sum t = (Sum t1) + vt by A6, A14, A15, RLVECT_1:38

.= (MorphsZQ V) . ((Sum s1) + vs) by AS, A6, A20, A22, defMorph

.= (MorphsZQ V) . (Sum s) by A12, A21, RLVECT_1:38 ; :: thesis: verum

hence for s being FinSequence of V

for t being FinSequence of (Z_MQ_VectSp V) 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 = (MorphsZQ V) . si ) ) holds

Sum t = (MorphsZQ V) . (Sum s) ; :: thesis: verum