let g1, g2 be FinSequence of REAL n; :: thesis: ( len f = len g1 & f . 1 = g1 . 1 & ( for i being Nat st 1 <= i & i < len f holds
g1 . (i + 1) = (g1 /. i) + (f /. (i + 1)) ) & len f = len g2 & f . 1 = g2 . 1 & ( for i being Nat st 1 <= i & i < len f holds
g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) ) implies g1 = g2 )
assume that
A28:
len f = len g1
and
A29:
f . 1 = g1 . 1
and
A30:
for i being Nat st 1 <= i & i < len f holds
g1 . (i + 1) = (g1 /. i) + (f /. (i + 1))
; :: thesis: ( not len f = len g2 or not f . 1 = g2 . 1 or ex i being Nat st
( 1 <= i & i < len f & not g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) ) or g1 = g2 )
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies g1 . $1 = g2 . $1 );
assume that
A31:
len f = len g2
and
A32:
f . 1 = g2 . 1
and
A33:
for i being Nat st 1 <= i & i < len f holds
g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))
; :: thesis: g1 = g2
A34:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A35:
S1[
k]
;
:: thesis: S1[k + 1]
( 1
<= k + 1 &
k + 1
<= len f implies
g1 . (k + 1) = g2 . (k + 1) )
proof
assume that
1
<= k + 1
and A36:
k + 1
<= len f
;
:: thesis: g1 . (k + 1) = g2 . (k + 1)
A37:
k < k + 1
by XREAL_1:31;
then A38:
k < len f
by A36, XXREAL_0:2;
per cases
( 1 <= k or 1 > k )
;
suppose A39:
1
<= k
;
:: thesis: g1 . (k + 1) = g2 . (k + 1)then A40:
g2 . (k + 1) = (g2 /. k) + (f /. (k + 1))
by A33, A38;
A41:
k <= len g2
by A31, A36, A37, XXREAL_0:2;
A42:
g1 /. k = g1 . k
by A28, A38, A39, FINSEQ_4:24;
g1 . (k + 1) = (g1 /. k) + (f /. (k + 1))
by A30, A38, A39;
hence
g1 . (k + 1) = g2 . (k + 1)
by A35, A36, A37, A39, A40, A42, A41, FINSEQ_4:24, XXREAL_0:2;
:: thesis: verum end;
end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
A43:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A43, A34);
hence
g1 = g2
by A28, A31, FINSEQ_1:18; :: thesis: verum