let V, W be Z_Module; :: thesis: for T being linear-transformation of V,W
for s being FinSequence of V
for t being FinSequence of W 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 = T . si ) ) holds
Sum t = T . (Sum s)
let T be linear-transformation of V,W; :: thesis: for s being FinSequence of V
for t being FinSequence of W 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 = T . si ) ) holds
Sum t = T . (Sum s)
XX: T is additive ;
defpred S₁[ Nat] means for s being FinSequence of V
for t being FinSequence of W 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 = T . si ) ) holds
Sum t = T . (Sum s);
A1: S₁[ 0 ]

proof

let s be FinSequence of V; :: thesis: for t being FinSequence of W 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 = T . si ) ) holds
Sum t = T . (Sum s)
let t be FinSequence of W; :: 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 = T . si ) ) implies Sum t = T . (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 = T . si ) ; :: thesis: Sum t = T . (Sum s)
s = <*> the carrier of V by A2;
then Sum s = 0. V by RLVECT_1:43;
then A3: T . (Sum s) = 0. W by ZMODUL05:19;
t = <*> the carrier of W by A2;
hence Sum t = T . (Sum s) by A3, RLVECT_1:43; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for s being FinSequence of V
for t being FinSequence of W 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 = T . si ) ) holds
Sum t = T . (Sum s)

let s be FinSequence of V; :: thesis: for t being FinSequence of W 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 = T . si ) ) holds
Sum t = T . (Sum s)
let t be FinSequence of W; :: 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 = T . si ) ) implies Sum t = T . (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 = T . si ) ; :: thesis: Sum t = T . (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 16;
reconsider t1 = t | k as FinSequence of W ;
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 16;
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 W ;
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 = T . 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 = T . si ) )
assume A18: i in dom s1 ; :: thesis: ex si being VECTOR of V st
( si = s1 . i & t1 . i = T . 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 = T . si ) by A7, A11, A8, A18;
take si ; :: thesis: ( si = s1 . i & t1 . i = T . si )
thus si = s1 . i by A12, A18, A19, FUNCT_1:49; :: thesis: t1 . i = T . si
thus t1 . i = T . si by A14, A11, A13, A18, A19, FUNCT_1:49; :: thesis: verum

end;

A20: Sum t1 = T . (Sum s1) by A5, A16, A17;
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) = T . ssi ) by A6, A7, A8, FINSEQ_1:4;
thus Sum t = (Sum t1) + vt by A6, A14, A15, RLVECT_1:38
.= T . ((Sum s1) + vs) by A6, A20, A22, XX
.= T . (Sum s) by A12, A21, RLVECT_1:38 ; :: thesis: verum

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
hence for s being FinSequence of V
for t being FinSequence of W 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 = T . si ) ) holds
Sum t = T . (Sum s) ; :: thesis: verum