let F, G be FinSequence of F_Complex ; :: thesis: ( len G = len F & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) implies Sum G = (Sum F) *' )
assume A1: ( len G = len F & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) ) ; :: thesis: Sum G = (Sum F) *'
defpred S₁[ Nat] means for F, G being FinSequence of F_Complex st len G = len F & len F = $1 & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) holds
Sum G = (Sum F) *' ;

now

let F, G be FinSequence of F_Complex ; :: thesis: ( len F = len G & len F = 0 & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) implies Sum G = (Sum F) *' )
assume A2: ( len F = len G & len F = 0 & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) ) ; :: thesis: Sum G = (Sum F) *'
then F = <*> the carrier of F_Complex by FINSEQ_1:32;
then Sum F = 0. F_Complex by RLVECT_1:60;
then A3: Sum F = (0. F_Complex ) *' by Lm2, Lm3;
G = <*> the carrier of F_Complex by A2, FINSEQ_1:32;
hence Sum G = (Sum F) *' by A3, RLVECT_1:60; :: thesis: verum

end;

then A4: S₁[ 0 ] ;

A5: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

now

let F, G be FinSequence of F_Complex ; :: thesis: ( len F = len G & len F = k + 1 & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) implies (Sum F) *' = Sum G )
assume A7: ( len F = len G & len F = k + 1 & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) ) ; :: thesis: (Sum F) *' = Sum G
set F1 = F | (Seg k);
reconsider F1 = F | (Seg k) as FinSequence by FINSEQ_1:19;
reconsider F1 = F1 as FinSequence of F_Complex by A7, Lm1;
set G1 = G | (Seg k);
reconsider G1 = G | (Seg k) as FinSequence by FINSEQ_1:19;
reconsider G1 = G1 as FinSequence of F_Complex by A7, Lm1;
A8: ( len G1 = k & len F1 = k ) by A7, Lm1;
A9: ( F = F1 ^ <*(F /. (k + 1))*> & G = G1 ^ <*(G /. (k + 1))*> ) by A7, Lm1;
A10: dom G = Seg (len F) by A7, FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3 ;
A11: dom G1 = Seg (len F1) by A8, FINSEQ_1:def 3
.= dom F1 by FINSEQ_1:def 3 ;

A12: now

let i be Element of NAT ; :: thesis: ( i in dom G1 implies G1 /. i = (F1 /. i) *' )
assume A13: i in dom G1 ; :: thesis: G1 /. i = (F1 /. i) *'
A14: dom G1 c= dom G by A7, Lm1;
then A15: F /. i = F . i by A10, A13, PARTFUN1:def 8
.= F1 . i by A9, A11, A13, FINSEQ_1:def 7
.= F1 /. i by A11, A13, PARTFUN1:def 8 ;
thus G1 /. i = G1 . i by A13, PARTFUN1:def 8
.= G . i by A9, A13, FINSEQ_1:def 7
.= G /. i by A13, A14, PARTFUN1:def 8
.= (F1 /. i) *' by A7, A13, A14, A15 ; :: thesis: verum

end;

1 <= k + 1 by NAT_1:11;
then A16: k + 1 in dom G by A7, FINSEQ_3:27;
thus (Sum F) *' = ((Sum F1) + (Sum <*(F /. (k + 1))*>)) *' by A9, RLVECT_1:58
.= ((Sum F1) *' ) + ((Sum <*(F /. (k + 1))*>) *' ) by COMPLFLD:87
.= (Sum G1) + ((Sum <*(F /. (k + 1))*>) *' ) by A6, A8, A12
.= (Sum G1) + ((F /. (k + 1)) *' ) by RLVECT_1:61
.= (Sum G1) + (G /. (k + 1)) by A7, A16
.= (Sum G1) + (Sum <*(G /. (k + 1))*>) by RLVECT_1:61
.= Sum G by A9, RLVECT_1:58 ; :: thesis: verum

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
hence Sum G = (Sum F) *' by A1; :: thesis: verum