let a, b, s be FinSequence of INT ; :: 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)) )
assume that
A1: len s > 0 and
A2: len a = len s and
A3: len b = len s and
A4: for n being Nat st 1 <= n & n <= len s holds
s . n = (a . n) + (b . n) and
A5: for k being Nat st 1 <= k & k < len s holds
b . k = - (a . (k + 1)) ; :: thesis: Sum s = (a . 1) + (b . (len s))
defpred S₁[ FinSequence of INT ] means ( len $1 > 0 implies for a, b being FinSequence of INT 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)) );
A6: S₁[ <*> INT ] ;
A7: for p being FinSequence of INT
for x being Element of INT st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of INT ; :: thesis: for x being Element of INT st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of INT ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A8: S₁[p] ; :: thesis: S₁[p ^ <*x*>]
set t = p ^ <*x*>;
assume len (p ^ <*x*>) > 0 ; :: thesis: for a, b being FinSequence of INT 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 INT ; :: 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
A9: len a = len (p ^ <*x*>) and
A10: len b = len (p ^ <*x*>) and
A11: for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) and
A12: 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*>)))
A13: Sum (p ^ <*x*>) = (Sum p) + x by GR_CY_1:20;

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

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

then B15: p = {} ;
A16: p ^ <*x*> = <*x*>

proof

p = {} by A14;
hence p ^ <*x*> = <*x*> by FINSEQ_1:47; :: thesis: verum

end;

then A17: len (p ^ <*x*>) = 1 by FINSEQ_1:56;
reconsider egy = 1 as Nat ;
egy <= len (p ^ <*x*>) by A16, FINSEQ_1:56;
then (p ^ <*x*>) . egy = (a . egy) + (b . egy) by A11;
hence Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A13, B15, A16, A17, FINSEQ_1:57, GR_CY_1:22; :: thesis: verum

end;

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

set m = len p;
set a' = a | (len p);
set b' = b | (len p);
A19: ( len p <= len a & len p <= len b ) by A9, A10, CALCUL_1:6;
then A20: len (a | (len p)) = len p by FINSEQ_1:80;
A21: len (b | (len p)) = len p by A19, FINSEQ_1:80;
A22: 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
A23: 1 <= n and
A24: n <= len p ; :: thesis: p . n = ((a | (len p)) . n) + ((b | (len p)) . n)
len p <= len (p ^ <*x*>) by CALCUL_1:6;
then A25: n <= len (p ^ <*x*>) by A24, XXREAL_0:2;
dom p = Seg (len p) by FINSEQ_1:def 3;
then A26: n in dom p by A23, A24, FINSEQ_1:3;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
p . n = (p ^ <*x*>) . n by A26, FINSEQ_1:def 7
.= (a . n) + (b . n) by A11, A23, A25
.= ((a | (len p)) . n) + (b . n) by A24, FINSEQ_3:121
.= ((a | (len p)) . n) + ((b | (len p)) . n) by A24, FINSEQ_3:121 ;
hence p . n = ((a | (len p)) . n) + ((b | (len p)) . n) ; :: thesis: verum

end;

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
A27: 1 <= n and
A28: n < len p ; :: thesis: (b | (len p)) . n = - ((a | (len p)) . (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A29: (b | (len p)) . n = b . n by A28, FINSEQ_3:121;
A30: n + 1 <= len p by A28, INT_1:20;
len p <= len (p ^ <*x*>) by CALCUL_1:6;
then A31: n < len (p ^ <*x*>) by A28, XXREAL_0:2;
(a | (len p)) . (n + 1) = a . (n + 1) by A30, FINSEQ_3:121;
hence (b | (len p)) . n = - ((a | (len p)) . (n + 1)) by A12, A27, A29, A31; :: thesis: verum

end;

then A32: Sum p = ((a | (len p)) . 1) + ((b | (len p)) . (len p)) by A8, A18, A20, A21, A22;
A33: (a | (len p)) . 1 = a . 1

proof

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

end;

x = (- ((b | (len p)) . (len p))) + (b . (len (p ^ <*x*>)))

proof

A34: len (p ^ <*x*>) = (len p) + 1

proof

len <*x*> = 1 by FINSEQ_1:56;
hence len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:35; :: thesis: verum

end;

A35: 1 <= len (p ^ <*x*>)

proof

0 + 1 = 1 ;
hence 1 <= len (p ^ <*x*>) by A34, XREAL_1:8; :: thesis: verum

end;

A36: a . (len (p ^ <*x*>)) = - ((b | (len p)) . (len p))

proof

A37: len p < len (p ^ <*x*>)

proof

0 + (len p) = len p ;
hence len p < len (p ^ <*x*>) by A34, XREAL_1:8; :: thesis: verum

end;

1 <= len p by A18, Lm1;
then A38: b . (len p) = - (a . ((len p) + 1)) by A12, A37;
b . (len p) = (b | (len p)) . (len p) by FINSEQ_3:121;
hence a . (len (p ^ <*x*>)) = - ((b | (len p)) . (len p)) by A34, A38; :: thesis: verum

end;

x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:59
.= (- ((b | (len p)) . (len p))) + (b . (len (p ^ <*x*>))) by A11, A34, A35, A36 ;
hence x = (- ((b | (len p)) . (len p))) + (b . (len (p ^ <*x*>))) ; :: thesis: verum

end;

hence Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A13, A32, A33; :: thesis: verum

end;

end;

end;

for p being FinSequence of INT holds S₁[p] from FINSEQ_2:sch 2(A6, A7);
hence Sum s = (a . 1) + (b . (len s)) by A1, A2, A3, A4, A5; :: thesis: verum