let V be ComplexLinearSpace; :: thesis: for z being Complex
for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) holds
Sum F = z * (Sum G)
let z be Complex; :: thesis: for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) holds
Sum F = z * (Sum G)
let F, G be FinSequence of the carrier of V; :: thesis: ( len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) implies Sum F = z * (Sum G) )
defpred S₁[ set ] means for H, I being FinSequence of the carrier of V st len H = len I & len H = $1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I);
A1: S₁[ 0 ]

proof

now

let H, I be FinSequence of the carrier of V; :: thesis: ( len H = len I & len H = 0 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) implies Sum H = z * (Sum I) )
assume that
A2: ( len H = len I & len H = 0 ) and
for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ; :: thesis: Sum H = z * (Sum I)
( Sum H = 0. V & Sum I = 0. V ) by A2, Lm2;
hence Sum H = z * (Sum I) by Th2; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

now

let n be Element of NAT ; :: thesis: ( ( for H, I being FinSequence of the carrier of V st len H = len I & len H = n & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I) ) implies for H, I being FinSequence of the carrier of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I) )
assume A4: for H, I being FinSequence of the carrier of V st len H = len I & len H = n & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I) ; :: thesis: for H, I being FinSequence of the carrier of V st len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) holds
Sum H = z * (Sum I)
let H, I be FinSequence of the carrier of V; :: thesis: ( len H = len I & len H = n + 1 & ( for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ) implies Sum H = z * (Sum I) )
assume that
A5: len H = len I and
A6: len H = n + 1 and
A7: for k being Element of NAT
for v being VECTOR of V st k in Seg (len H) & v = I . k holds
H . k = z * v ; :: thesis: Sum H = z * (Sum I)
reconsider p = H | (Seg n), q = I | (Seg n) as FinSequence of the carrier of V 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: now

let k be Element of NAT ; :: thesis: for v being VECTOR of V st k in Seg (len p) & v = q . k holds
p . k = z * v
let v be VECTOR of V; :: thesis: ( k in Seg (len p) & v = q . k implies p . k = z * v )
assume that
A11: k in Seg (len p) and
A12: v = q . k ; :: thesis: p . k = z * v
len p <= len H by A6, A8, FINSEQ_1:21;
then A13: Seg (len p) c= Seg (len H) by FINSEQ_1:7;
dom q = Seg n by A5, A6, A8, FINSEQ_1:21;
then I . k = q . k by A9, A11, FUNCT_1:70;
then A14: H . k = z * v by A7, A11, A12, A13;
dom p = Seg n by A6, A8, FINSEQ_1:21;
hence p . k = z * v by A9, A11, A14, FUNCT_1:70; :: thesis: verum

end;

n + 1 in Seg (n + 1) by FINSEQ_1:6;
then ( n + 1 in dom H & n + 1 in dom I ) by A5, A6, FINSEQ_1:def 3;
then reconsider v1 = H . (n + 1), v2 = I . (n + 1) as VECTOR of V by FUNCT_1:172;
A15: v1 = z * v2 by A6, A7, FINSEQ_1:6;
A16: dom q = Seg (len q) by FINSEQ_1:def 3;
dom p = Seg (len p) by FINSEQ_1:def 3;
hence Sum H = (Sum p) + v1 by A6, A9, RLVECT_1:55
.= (z * (Sum q)) + (z * v2) by A4, A9, A10, A15
.= z * ((Sum q) + v2) by Def2
.= z * (Sum I) by A5, A6, A9, A16, RLVECT_1:55 ;
:: thesis: verum

end;

hence for n being Element of NAT st S₁[n] holds
S₁[n + 1] ; :: thesis: verum

end;

A17: dom F = Seg (len F) by FINSEQ_1:def 3;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A3);
hence ( len F = len G & ( for k being Element of NAT
for v being VECTOR of V st k in dom F & v = G . k holds
F . k = z * v ) implies Sum F = z * (Sum G) ) by A17; :: thesis: verum