defpred S1[ set ] means for F being FinSequence of the carrier of V st len F = $1 holds
ex u being Element of V ex f being Function of NAT ,the carrier of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) );
A1: S1[ 0 ]
proof
now
let F be FinSequence of the carrier of V; :: thesis: ( len F = 0 implies ex u being Element of the carrier of V ex f' being Function of NAT ,the carrier of V st
( u = f' . (len F) & f' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v ) ) )
assume A2: len F = 0 ; :: thesis: ex u being Element of the carrier of V ex f' being Function of NAT ,the carrier of V st
( u = f' . (len F) & f' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v ) )
reconsider f = NAT --> (0. V) as Function of NAT ,the carrier of V ;
take u = f . (len F); :: thesis: ex f' being Function of NAT ,the carrier of V st
( u = f' . (len F) & f' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v ) )
take f' = f; :: thesis: ( u = f' . (len F) & f' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v ) )
thus ( u = f' . (len F) & f' . 0 = 0. V ) by FUNCOP_1:13; :: thesis: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v
let j be Element of NAT ; :: thesis: for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v
thus for v being Element of V st j < len F & v = F . (j + 1) holds
f' . (j + 1) = (f' . j) + v by A2; :: thesis: verum
end;
hence S1[ 0 ] ; :: thesis: verum
end;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
now
let n be Element of NAT ; :: thesis: ( ( for F being FinSequence of the carrier of V st len F = n holds
ex u being Element of V ex f being Function of NAT ,the carrier of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) ) implies for F being FinSequence of the carrier of V st len F = n + 1 holds
ex z being Element of the carrier of V ex f'' being Function of NAT ,the carrier of V st
( z = f'' . (len F) & f'' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v ) ) )
assume A4: for F being FinSequence of the carrier of V st len F = n holds
ex u being Element of V ex f being Function of NAT ,the carrier of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) ; :: thesis: for F being FinSequence of the carrier of V st len F = n + 1 holds
ex z being Element of the carrier of V ex f'' being Function of NAT ,the carrier of V st
( z = f'' . (len F) & f'' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v ) )
let F be FinSequence of the carrier of V; :: thesis: ( len F = n + 1 implies ex z being Element of the carrier of V ex f'' being Function of NAT ,the carrier of V st
( z = f'' . (len F) & f'' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v ) ) )
assume A5: len F = n + 1 ; :: thesis: ex z being Element of the carrier of V ex f'' being Function of NAT ,the carrier of V st
( z = f'' . (len F) & f'' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v ) )
reconsider G = F | (Seg n) as FinSequence of the carrier of V by FINSEQ_1:23;
A6: n < n + 1 by NAT_1:13;
then A7: len G = n by A5, FINSEQ_1:21;
then consider u being Element of V, f being Function of NAT ,the carrier of V such that
u = f . (len G) and
A8: f . 0 = 0. V and
A9: for j being Element of NAT
for v being Element of V st j < len G & v = G . (j + 1) holds
f . (j + 1) = (f . j) + v by A4;
dom F = Seg (n + 1) by A5, FINSEQ_1:def 3;
then n + 1 in dom F by FINSEQ_1:6;
then ( F . (n + 1) in rng F & rng F c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider u1 = F . (n + 1) as Element of V ;
defpred S2[ set , set ] means for j being Element of 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 ) );
A10: for k being Element of NAT ex v being Element of V st S2[k,v]
proof
let k be Element of NAT ; :: thesis: ex v being Element of V st S2[k,v]
reconsider i = k as Element of NAT ;
A11: now
assume A12: i < n + 1 ; :: thesis: ex v being Element of the carrier of V st
for j being Element of 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; :: thesis: for j being Element of 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 Element of NAT ; :: thesis: ( 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 A13: k = j ; :: thesis: ( ( 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 ) ; :: thesis: ( 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 A12, A13; :: thesis: verum
end;
now
assume A14: n + 1 <= i ; :: thesis: ex v being Element of the carrier of V st
for j being Element of 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; :: thesis: for j being Element of 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 Element of NAT ; :: thesis: ( 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 ; :: thesis: ( ( 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 A14; :: thesis: ( 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 ; :: thesis: for u2 being Element of V st u2 = F . (n + 1) holds
v = (f . (len G)) + u2
let u2 be Element of V; :: thesis: ( u2 = F . (n + 1) implies v = (f . (len G)) + u2 )
assume u2 = F . (n + 1) ; :: thesis: v = (f . (len G)) + u2
hence v = (f . (len G)) + u2 ; :: thesis: verum
end;
hence ex v being Element of V st S2[k,v] by A11; :: thesis: verum
end;
consider f' being Function of NAT ,the carrier of V such that
A15: for k being Element of NAT holds S2[k,f' . k] from FUNCT_2:sch 3(A10);
take z = f' . (n + 1); :: thesis: ex f'' being Function of NAT ,the carrier of V st
( z = f'' . (len F) & f'' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v ) )
take f'' = f'; :: thesis: ( z = f'' . (len F) & f'' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v ) )
thus z = f'' . (len F) by A5; :: thesis: ( f'' . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v ) )
thus f'' . 0 = 0. V by A8, A15; :: thesis: for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v
let j be Element of NAT ; :: thesis: for v being Element of V st j < len F & v = F . (j + 1) holds
f'' . (j + 1) = (f'' . j) + v
let v be Element of V; :: thesis: ( j < len F & v = F . (j + 1) implies f'' . (j + 1) = (f'' . j) + v )
assume that
A16: j < len F and
A17: v = F . (j + 1) ; :: thesis: f'' . (j + 1) = (f'' . j) + v
A18: now
assume A19: j < n ; :: thesis: f'' . (j + 1) = (f'' . j) + v
then A20: ( j <= n & 1 <= 1 + j ) by NAT_1:11;
( 1 <= j + 1 & j + 1 <= n + 1 ) by A19, NAT_1:11, XREAL_1:9;
then ( j + 1 in Seg (n + 1) & j + 1 <= n ) by A19, FINSEQ_1:3, NAT_1:13;
then ( j + 1 in dom F & j + 1 in Seg n ) by A5, A20, FINSEQ_1:3, FINSEQ_1:def 3;
then ( v = G . (j + 1) & j < len G ) by A5, A6, A17, A19, FINSEQ_1:21, FUNCT_1:72;
then ( f . (j + 1) = (f . j) + v & j < n + 1 ) by A9, A19, NAT_1:13;
then ( f . (j + 1) = (f' . j) + v & j + 1 < n + 1 ) by A15, A19, XREAL_1:8;
hence f'' . (j + 1) = (f'' . j) + v by A15; :: thesis: verum
end;
A21: now
assume A22: j = n ; :: thesis: f'' . (j + 1) = (f'' . j) + v
then f'' . (j + 1) = (f . j) + v by A7, A15, A17;
hence f'' . (j + 1) = (f'' . j) + v by A6, A15, A22; :: thesis: verum
end;
j <= n by A5, A16, NAT_1:13;
hence f'' . (j + 1) = (f'' . j) + v by A18, A21, XXREAL_0:1; :: thesis: verum
end;
hence for n being Element of NAT st S1[n] holds
S1[n + 1] ; :: thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A1, A3);
 then consider u being Element of V such that
A23: ex f being Function of NAT ,the carrier of V st
( u = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) ;
thus ex b1 being Element of V ex f being Function of NAT ,the carrier of V st
( b1 = f . (len F) & f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by A23; :: thesis: verum