defpred S1[ set ] means for F being the carrier of V -valued FinSequence st len F = $1 holds
ex u being Element of V ex f being sequence of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) );
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
for
F being the
carrier of
V -valued FinSequence st
len F = n holds
ex
u being
Element of
V ex
f being
sequence of
V st
(
u = f . (len F) &
f . 0 = 0. V & ( for
j being
Nat for
v being
Element of
V st
j < len F &
v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
;
S1[n + 1]
let F be the
carrier of
V -valued FinSequence;
( len F = n + 1 implies ex u being Element of V ex f being sequence of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) )
A3:
rng F c= the
carrier of
V
by RELAT_1:def 19;
then reconsider F1 =
F as
FinSequence of
V by FINSEQ_1:def 4;
reconsider G =
F1 | (Seg n) as
FinSequence of
V by FINSEQ_1:18;
assume A4:
len F = n + 1
;
ex u being Element of V ex f being sequence of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
then
dom F = Seg (n + 1)
by FINSEQ_1:def 3;
then
n + 1
in dom F
by FINSEQ_1:4;
then
F . (n + 1) in rng F
by FUNCT_1:def 3;
then reconsider u1 =
F . (n + 1) as
Element of
V by A3;
A5:
n < n + 1
by NAT_1:13;
then consider u being
Element of
V,
f being
sequence of
V such that
u = f . (len G)
and A6:
f . 0 = 0. V
and A7:
for
j being
Nat for
v being
Element of
V st
j < len G &
v = G . (j + 1) holds
f . (j + 1) = (f . j) + v
by A2, A4, FINSEQ_1:17;
defpred S2[
set ,
set ]
means for
j being
Nat st $1
= j holds
( (
j < n + 1 implies $2
= f . $1 ) & (
n + 1
<= j implies for
u being
Element of
V st
u = F . (n + 1) holds
$2
= (f . (len G)) + u ) );
A8:
for
k being
Element of
NAT ex
v being
Element of
V st
S2[
k,
v]
proof
let k be
Element of
NAT ;
ex v being Element of V st S2[k,v]
reconsider i =
k as
Element of
NAT ;
A9:
now ( n + 1 <= i implies ex v being Element of the carrier of V st
for j being Nat st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) ) )assume A10:
n + 1
<= i
;
ex v being Element of the carrier of V st
for j being Nat st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) )take v =
(f . (len G)) + u1;
for j being Nat st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) )let j be
Nat;
( k = j implies ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) ) )assume
k = j
;
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 ) )hence
(
j < n + 1 implies
v = f . k )
by A10;
( n + 1 <= j implies for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2 )assume
n + 1
<= j
;
for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2let u2 be
Element of
V;
( u2 = F . (n + 1) implies v = (f . (len G)) + u2 )assume
u2 = F . (n + 1)
;
v = (f . (len G)) + u2hence
v = (f . (len G)) + u2
;
verum end;
now ( i < n + 1 implies ex v being Element of the carrier of V st
for j being Nat st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) ) )assume A11:
i < n + 1
;
ex v being Element of the carrier of V st
for j being Nat st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) )take v =
f . k;
for j being Nat st k = j holds
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) )let j be
Nat;
( k = j implies ( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) ) )assume A12:
k = j
;
( ( j < n + 1 implies v = f . k ) & ( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u ) )thus
(
j < n + 1 implies
v = f . k )
;
( n + 1 <= j implies for u being Element of V st u = F . (n + 1) holds
v = (f . (len G)) + u )thus
(
n + 1
<= j implies for
u being
Element of
V st
u = F . (n + 1) holds
v = (f . (len G)) + u )
by A11, A12;
verum end;
hence
ex
v being
Element of
V st
S2[
k,
v]
by A9;
verum
end;
consider f9 being
sequence of the
carrier of
V such that A13:
for
k being
Element of
NAT holds
S2[
k,
f9 . k]
from FUNCT_2:sch 3(A8);
A14:
for
k being
Nat holds
S2[
k,
f9 . k]
take z =
f9 . (n + 1);
ex f being sequence of V st
( z = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
take f99 =
f9;
( z = f99 . (len F) & f99 . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + v ) )
thus
z = f99 . (len F)
by A4;
( f99 . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + v ) )
thus
f99 . 0 = 0. V
by A6, A14;
for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + v
let j be
Nat;
for v being Element of V st j < len F & v = F . (j + 1) holds
f99 . (j + 1) = (f99 . j) + vlet v be
Element of
V;
( j < len F & v = F . (j + 1) implies f99 . (j + 1) = (f99 . j) + v )
assume that A15:
j < len F
and A16:
v = F . (j + 1)
;
f99 . (j + 1) = (f99 . j) + v
A17:
len G = n
by A4, A5, FINSEQ_1:17;
A18:
now ( j = n implies f99 . (j + 1) = (f99 . j) + v )end;
A20:
now ( j < n implies f99 . (j + 1) = (f99 . j) + v )assume A21:
j < n
;
f99 . (j + 1) = (f99 . j) + vthen A22:
j + 1
< n + 1
by XREAL_1:6;
( 1
<= 1
+ j &
j + 1
<= n )
by A21, NAT_1:11, NAT_1:13;
then
j + 1
in Seg n
by FINSEQ_1:1;
then A23:
v = G . (j + 1)
by A16, FUNCT_1:49;
j < len G
by A4, A5, A21, FINSEQ_1:17;
then A24:
f . (j + 1) = (f . j) + v
by A7, A23;
j < n + 1
by A21, NAT_1:13;
then
f . (j + 1) = (f9 . j) + v
by A14, A24;
hence
f99 . (j + 1) = (f99 . j) + v
by A14, A22;
verum end;
j <= n
by A4, A15, NAT_1:13;
hence
f99 . (j + 1) = (f99 . j) + v
by A20, A18, XXREAL_0:1;
verum
end;
A25:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A25, A1);
hence
ex b1 being Element of V ex f being sequence of V st
( b1 = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) )
; verum