let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K

for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let V1 be finite-dimensional VectSp of K; :: thesis: for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let a be Element of V1; :: thesis: for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let F be FinSequence of V1; :: thesis: for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let G be FinSequence of K; :: thesis: ( len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) implies Sum F = (Sum G) * a )

defpred S_{1}[ Nat] means for H being FinSequence of V1

for I being FinSequence of K st len H = len I & len H = $1 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a;

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A17, A1);

hence ( len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) implies Sum F = (Sum G) * a ) ; :: thesis: verum

for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let V1 be finite-dimensional VectSp of K; :: thesis: for a being Element of V1

for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let a be Element of V1; :: thesis: for F being FinSequence of V1

for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let F be FinSequence of V1; :: thesis: for G being FinSequence of K st len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) holds

Sum F = (Sum G) * a

let G be FinSequence of K; :: thesis: ( len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) implies Sum F = (Sum G) * a )

defpred S

for I being FinSequence of K st len H = len I & len H = $1 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a;

A1: for n being Nat st S

S

proof

A17:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: for H being FinSequence of V1

for I being FinSequence of K st len H = len I & len H = n & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a ; :: thesis: S_{1}[n + 1]

let H be FinSequence of V1; :: thesis: for I being FinSequence of K st len H = len I & len H = n + 1 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a

let I be FinSequence of K; :: thesis: ( len H = len I & len H = n + 1 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) implies Sum H = (Sum I) * a )

assume that

A3: len H = len I and

A4: len H = n + 1 and

A5: for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ; :: thesis: Sum H = (Sum I) * a

reconsider q = I | (Seg n) as FinSequence of K by FINSEQ_1:18;

reconsider p = H | (Seg n) as FinSequence of V1 by FINSEQ_1:18;

A6: n <= n + 1 by NAT_1:12;

then A7: len p = n by A4, FINSEQ_1:17;

A8: dom p = Seg n by A4, A6, FINSEQ_1:17;

A9: len q = n by A3, A4, A6, FINSEQ_1:17;

A10: dom q = Seg n by A3, A4, A6, FINSEQ_1:17;

n + 1 in Seg (n + 1) by FINSEQ_1:4;

then A15: n + 1 in dom H by A4, FINSEQ_1:def 3;

then reconsider v1 = H . (n + 1) as Element of V1 by FINSEQ_2:11;

dom H = dom I by A3, FINSEQ_3:29;

then reconsider v2 = I . (n + 1) as Element of K by A15, FINSEQ_2:11;

A16: v1 = v2 * a by A5, A15;

thus Sum H = (Sum p) + v1 by A4, A7, A8, RLVECT_1:38

.= ((Sum q) * a) + (v2 * a) by A2, A7, A9, A11, A16

.= ((Sum q) + v2) * a by VECTSP_1:def 15

.= (Sum I) * a by A3, A4, A9, A10, RLVECT_1:38 ; :: thesis: verum

end;assume A2: for H being FinSequence of V1

for I being FinSequence of K st len H = len I & len H = n & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a ; :: thesis: S

let H be FinSequence of V1; :: thesis: for I being FinSequence of K st len H = len I & len H = n + 1 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a

let I be FinSequence of K; :: thesis: ( len H = len I & len H = n + 1 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) implies Sum H = (Sum I) * a )

assume that

A3: len H = len I and

A4: len H = n + 1 and

A5: for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ; :: thesis: Sum H = (Sum I) * a

reconsider q = I | (Seg n) as FinSequence of K by FINSEQ_1:18;

reconsider p = H | (Seg n) as FinSequence of V1 by FINSEQ_1:18;

A6: n <= n + 1 by NAT_1:12;

then A7: len p = n by A4, FINSEQ_1:17;

A8: dom p = Seg n by A4, A6, FINSEQ_1:17;

A9: len q = n by A3, A4, A6, FINSEQ_1:17;

A10: dom q = Seg n by A3, A4, A6, FINSEQ_1:17;

A11: now :: thesis: for k being Nat

for v being Element of K st k in dom p & v = q . k holds

p . k = v * a

reconsider n = n as Element of NAT by ORDINAL1:def 12;for v being Element of K st k in dom p & v = q . k holds

p . k = v * a

len p <= len H
by A4, A6, FINSEQ_1:17;

then A12: dom p c= dom H by FINSEQ_3:30;

let k be Nat; :: thesis: for v being Element of K st k in dom p & v = q . k holds

p . k = v * a

let v be Element of K; :: thesis: ( k in dom p & v = q . k implies p . k = v * a )

assume that

A13: k in dom p and

A14: v = q . k ; :: thesis: p . k = v * a

I . k = q . k by A8, A10, A13, FUNCT_1:47;

then H . k = v * a by A5, A13, A14, A12;

hence p . k = v * a by A13, FUNCT_1:47; :: thesis: verum

end;then A12: dom p c= dom H by FINSEQ_3:30;

let k be Nat; :: thesis: for v being Element of K st k in dom p & v = q . k holds

p . k = v * a

let v be Element of K; :: thesis: ( k in dom p & v = q . k implies p . k = v * a )

assume that

A13: k in dom p and

A14: v = q . k ; :: thesis: p . k = v * a

I . k = q . k by A8, A10, A13, FUNCT_1:47;

then H . k = v * a by A5, A13, A14, A12;

hence p . k = v * a by A13, FUNCT_1:47; :: thesis: verum

n + 1 in Seg (n + 1) by FINSEQ_1:4;

then A15: n + 1 in dom H by A4, FINSEQ_1:def 3;

then reconsider v1 = H . (n + 1) as Element of V1 by FINSEQ_2:11;

dom H = dom I by A3, FINSEQ_3:29;

then reconsider v2 = I . (n + 1) as Element of K by A15, FINSEQ_2:11;

A16: v1 = v2 * a by A5, A15;

thus Sum H = (Sum p) + v1 by A4, A7, A8, RLVECT_1:38

.= ((Sum q) * a) + (v2 * a) by A2, A7, A9, A11, A16

.= ((Sum q) + v2) * a by VECTSP_1:def 15

.= (Sum I) * a by A3, A4, A9, A10, RLVECT_1:38 ; :: thesis: verum

proof

for n being Nat holds S
let H be FinSequence of V1; :: thesis: for I being FinSequence of K st len H = len I & len H = 0 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a

let I be FinSequence of K; :: thesis: ( len H = len I & len H = 0 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) implies Sum H = (Sum I) * a )

assume that

A18: len H = len I and

A19: len H = 0 and

for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ; :: thesis: Sum H = (Sum I) * a

H = <*> the carrier of V1 by A19;

then A20: Sum H = 0. V1 by RLVECT_1:43;

I = <*> the carrier of K by A18, A19;

then Sum I = 0. K by RLVECT_1:43;

hence Sum H = (Sum I) * a by A20, VECTSP_1:14; :: thesis: verum

end;for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) holds

Sum H = (Sum I) * a

let I be FinSequence of K; :: thesis: ( len H = len I & len H = 0 & ( for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ) implies Sum H = (Sum I) * a )

assume that

A18: len H = len I and

A19: len H = 0 and

for k being Nat

for v being Element of K st k in dom H & v = I . k holds

H . k = v * a ; :: thesis: Sum H = (Sum I) * a

H = <*> the carrier of V1 by A19;

then A20: Sum H = 0. V1 by RLVECT_1:43;

I = <*> the carrier of K by A18, A19;

then Sum I = 0. K by RLVECT_1:43;

hence Sum H = (Sum I) * a by A20, VECTSP_1:14; :: thesis: verum

hence ( len F = len G & ( for k being Nat

for v being Element of K st k in dom F & v = G . k holds

F . k = v * a ) implies Sum F = (Sum G) * a ) ; :: thesis: verum