defpred S₁[ FinSequence of COMPLEX ] means ( len $1 > 0 implies for a, b being FinSequence of COMPLEX st len a = len $1 & len b = len $1 & ( for n being Nat st 1 <= n & n <= len $1 holds
$1 . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len $1 holds
b . k = - (a . (k + 1)) ) holds
Sum $1 = (a . 1) + (b . (len $1)) );
A1: for p being FinSequence of COMPLEX
for x being Element of COMPLEX st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of COMPLEX ; :: thesis: for x being Element of COMPLEX st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of COMPLEX ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A2: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
set t = p ^ <*x*>;
assume len (p ^ <*x*>) > 0 ; :: thesis: for a, b being FinSequence of COMPLEX st len a = len (p ^ <*x*>) & len b = len (p ^ <*x*>) & ( for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ) holds
Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
let a, b be FinSequence of COMPLEX ; :: thesis: ( len a = len (p ^ <*x*>) & len b = len (p ^ <*x*>) & ( for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ) implies Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) )
assume that
A3: len a = len (p ^ <*x*>) and
A4: len b = len (p ^ <*x*>) and
A5: for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) and
A6: for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ; :: thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
A7: Sum (p ^ <*x*>) = (Sum p) + x by RVSUM_2:31;

per cases ( len p = 0 or len p > 0 ) ;

suppose A8: len p = 0 ; :: thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))

reconsider egy = 1 as Nat ;
p = {} by A8;
then A9: p ^ <*x*> = <*x*> by FINSEQ_1:34;
then egy <= len (p ^ <*x*>) by FINSEQ_1:39;
then A10: (p ^ <*x*>) . egy = (a . egy) + (b . egy) by A5;
A11: p = {} by A8;
len (p ^ <*x*>) = 1 by A9, FINSEQ_1:39;
hence Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A7, A11, A9, A10, GR_CY_1:3; :: thesis: verum

end;

suppose A12: len p > 0 ; :: thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))

set m = len p;
set a9 = a | (len p);
A13: (a | (len p)) . 1 = a . 1

proof

reconsider egy = 1 as Element of NAT ;
0 + 1 = 1 ;
then egy <= len p by A12, INT_1:7;
hence (a | (len p)) . 1 = a . 1 by FINSEQ_3:112; :: thesis: verum

end;

set b9 = b | (len p);
A14: b . (len p) = (b | (len p)) . (len p) by FINSEQ_3:112;
A15: for n being Nat st 1 <= n & n < len p holds
(b | (len p)) . n = - ((a | (len p)) . (n + 1))

proof

let n be Nat; :: thesis: ( 1 <= n & n < len p implies (b | (len p)) . n = - ((a | (len p)) . (n + 1)) )
assume that
A16: 1 <= n and
A17: n < len p ; :: thesis: (b | (len p)) . n = - ((a | (len p)) . (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A18: (b | (len p)) . n = b . n by A17, FINSEQ_3:112;
n + 1 <= len p by A17, INT_1:7;
then A19: (a | (len p)) . (n + 1) = a . (n + 1) by FINSEQ_3:112;
len p <= len (p ^ <*x*>) by CALCUL_1:6;
then n < len (p ^ <*x*>) by A17, XXREAL_0:2;
hence (b | (len p)) . n = - ((a | (len p)) . (n + 1)) by A6, A16, A18, A19; :: thesis: verum

end;

A20: for n being Nat st 1 <= n & n <= len p holds
p . n = ((a | (len p)) . n) + ((b | (len p)) . n)

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len p implies p . n = ((a | (len p)) . n) + ((b | (len p)) . n) )
assume that
A21: 1 <= n and
A22: n <= len p ; :: thesis: p . n = ((a | (len p)) . n) + ((b | (len p)) . n)
dom p = Seg (len p) by FINSEQ_1:def 3;
then A23: n in dom p by A21, A22;
len p <= len (p ^ <*x*>) by CALCUL_1:6;
then A24: n <= len (p ^ <*x*>) by A22, XXREAL_0:2;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
p . n = (p ^ <*x*>) . n by A23, FINSEQ_1:def 7
.= (a . n) + (b . n) by A5, A21, A24
.= ((a | (len p)) . n) + (b . n) by A22, FINSEQ_3:112
.= ((a | (len p)) . n) + ((b | (len p)) . n) by A22, FINSEQ_3:112 ;
hence p . n = ((a | (len p)) . n) + ((b | (len p)) . n) ; :: thesis: verum

end;

A25: 1 <= len p by A12, Lm1;
len <*x*> = 1 by FINSEQ_1:39;
then A26: len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:22;
0 + (len p) = len p ;
then len p < len (p ^ <*x*>) by A26, XREAL_1:6;
then A27: b . (len p) = - (a . ((len p) + 1)) by A6, A25;
0 + 1 = 1 ;
then A28: 1 <= len (p ^ <*x*>) by A26, XREAL_1:6;
A29: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42
.= (- ((b | (len p)) . (len p))) + (b . (len (p ^ <*x*>))) by A5, A26, A28, A27, A14 ;
len p <= len b by A4, CALCUL_1:6;
then A30: len (b | (len p)) = len p by FINSEQ_1:59;
len p <= len a by A3, CALCUL_1:6;
then len (a | (len p)) = len p by FINSEQ_1:59;
then Sum p = ((a | (len p)) . 1) + ((b | (len p)) . (len p)) by A2, A12, A30, A20, A15;
hence Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A7, A13, A29; :: thesis: verum

end;

end;

end;

A31: S₁[ <*> COMPLEX] ;
A32: for p being FinSequence of COMPLEX holds S₁[p] from FINSEQ_2:sch 2(A31, A1);
let a, b, s be complex-valued FinSequence; :: thesis: ( len s > 0 & len a = len s & len b = len s & ( for n being Nat st 1 <= n & n <= len s holds
s . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len s holds
b . k = - (a . (k + 1)) ) implies Sum s = (a . 1) + (b . (len s)) )
A33: ( a is FinSequence of COMPLEX & b is FinSequence of COMPLEX & s is FinSequence of COMPLEX ) by FINSEQ_1:107;
assume ( len s > 0 & len a = len s & len b = len s & ( for n being Nat st 1 <= n & n <= len s holds
s . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len s holds
b . k = - (a . (k + 1)) ) ) ; :: thesis: Sum s = (a . 1) + (b . (len s))
hence Sum s = (a . 1) + (b . (len s)) by A32, A33; :: thesis: verum