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_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

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

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

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

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

proof

A3:
for k being Nat st S
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;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

S

proof

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

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

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

end;assume A4: S

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

hence
Sex 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 15;

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 )

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

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

A15:
ZMtoMQV (V,p,(Sum s1)) in Lin IQ
by A4, A11, A12;
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;( 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

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

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

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

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

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