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₁[ 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: S₁[ 0 ]

proof

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
A2: ( len H = len I & 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 & I = <*> the carrier of K ) by A2;
then ( Sum H = 0. V1 & Sum I = 0. K ) by RLVECT_1:60;
hence Sum H = (Sum I) * a by VECTSP_1:59; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: 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₁[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
A5: len H = len I and
A6: len H = n + 1 and
A7: 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 p = H | (Seg n) as FinSequence of V1 by FINSEQ_1:23;
reconsider q = I | (Seg n) as FinSequence of K by FINSEQ_1:23;
A8: n <= n + 1 by NAT_1:12;
then A9: ( len p = n & len q = n ) by A5, A6, FINSEQ_1:21;
A10: ( dom p = Seg n & dom q = Seg n ) by A5, A6, A8, FINSEQ_1:21;

A11: now

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
A12: k in dom p and
A13: v = q . k ; :: thesis: p . k = v * a
len p <= len H by A6, A8, FINSEQ_1:21;
then A14: dom p c= dom H by FINSEQ_3:32;
I . k = q . k by A10, A12, FUNCT_1:70;
then H . k = v * a by A7, A12, A13, A14;
hence p . k = v * a by A12, FUNCT_1:70; :: thesis: verum

end;

reconsider n = n as Element of NAT by ORDINAL1:def 13;
n + 1 in Seg (n + 1) by FINSEQ_1:6;
then A15: n + 1 in dom H by A6, FINSEQ_1:def 3;
then reconsider v1 = H . (n + 1) as Element of V1 by FINSEQ_2:13;
dom H = dom I by A5, FINSEQ_3:31;
then reconsider v2 = I . (n + 1) as Element of K by A15, FINSEQ_2:13;
A16: v1 = v2 * a by A7, A15;
thus Sum H = (Sum p) + v1 by A6, A9, A10, RLVECT_1:55
.= ((Sum q) * a) + (v2 * a) by A4, A9, A11, A16
.= ((Sum q) + v2) * a by VECTSP_1:def 26
.= (Sum I) * a by A5, A6, A9, A10, RLVECT_1:55 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
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