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) *' ;
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 that
A1: len G = len F and
A2: for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ; :: thesis: Sum G = (Sum F) *'

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

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

now :: thesis: for F, G being FinSequence of F_Complex st len F = len G & len F = k + 1 & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) holds
(Sum F) *' = Sum G

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 that
A5: len F = len G and
A6: len F = k + 1 and
A7: for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ; :: thesis: (Sum F) *' = Sum G
set G1 = G | (Seg k);
reconsider G1 = G | (Seg k) as FinSequence by FINSEQ_1:15;
reconsider G1 = G1 as FinSequence of F_Complex by A5, A6, Lm1;
A8: G = G1 ^ <*(G /. (k + 1))*> by A5, A6, Lm1;
set F1 = F | (Seg k);
reconsider F1 = F | (Seg k) as FinSequence by FINSEQ_1:15;
reconsider F1 = F1 as FinSequence of F_Complex by A6, Lm1;
A9: len F1 = k by A6, Lm1;
A10: len G1 = k by A5, A6, Lm1;
then A11: dom G1 = Seg (len F1) by A9, FINSEQ_1:def 3
.= dom F1 by FINSEQ_1:def 3 ;
1 <= k + 1 by NAT_1:11;
then A12: k + 1 in dom G by A5, A6, FINSEQ_3:25;
A13: F = F1 ^ <*(F /. (k + 1))*> by A6, Lm1;
A14: dom G = Seg (len F) by A5, FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3 ;

A15: now :: thesis: for i being Element of NAT st i in dom G1 holds
G1 /. i = (F1 /. i) *'

let i be Element of NAT ; :: thesis: ( i in dom G1 implies G1 /. i = (F1 /. i) *' )
assume A16: i in dom G1 ; :: thesis: G1 /. i = (F1 /. i) *'
A17: dom G1 c= dom G by A5, A6, Lm1;
then A18: F /. i = F . i by A14, A16, PARTFUN1:def 6
.= F1 . i by A13, A11, A16, FINSEQ_1:def 7
.= F1 /. i by A11, A16, PARTFUN1:def 6 ;
thus G1 /. i = G1 . i by A16, PARTFUN1:def 6
.= G . i by A8, A16, FINSEQ_1:def 7
.= G /. i by A16, A17, PARTFUN1:def 6
.= (F1 /. i) *' by A7, A16, A17, A18 ; :: thesis: verum

end;

thus (Sum F) *' = ((Sum F1) + (Sum <*(F /. (k + 1))*>)) *' by A13, RLVECT_1:41
.= ((Sum F1) *') + ((Sum <*(F /. (k + 1))*>) *') by COMPLFLD:51
.= (Sum G1) + ((Sum <*(F /. (k + 1))*>) *') by A4, A10, A9, A15
.= (Sum G1) + ((F /. (k + 1)) *') by RLVECT_1:44
.= (Sum G1) + (G /. (k + 1)) by A7, A12
.= (Sum G1) + (Sum <*(G /. (k + 1))*>) by RLVECT_1:44
.= Sum G by A8, RLVECT_1:41 ; :: thesis: verum

end;

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

end;

now :: thesis: for F, G being FinSequence of F_Complex st len F = len G & len F = 0 & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) holds
Sum G = (Sum F) *'

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 that
A19: len F = len G and
A20: len F = 0 and
for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ; :: thesis: Sum G = (Sum F) *'
F = <*> the carrier of F_Complex by A20;
then Sum F = 0. F_Complex by RLVECT_1:43;
then A21: Sum F = (0. F_Complex) *' by Lm2, COMPLEX1:38;
G = <*> the carrier of F_Complex by A19, A20;
hence Sum G = (Sum F) *' by A21, RLVECT_1:43; :: thesis: verum

end;

then A22: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A22, A3);
hence Sum G = (Sum F) *' by A1, A2; :: thesis: verum