A2:
for n being Nat st 1 <= n & n < len prg holds
for x being Element of ND (V,A) ex y being Element of ND (V,A) st S1[n,x,y]
proof
let n be
Nat;
( 1 <= n & n < len prg implies for x being Element of ND (V,A) ex y being Element of ND (V,A) st S1[n,x,y] )
assume
( 1
<= n &
n < len prg )
;
for x being Element of ND (V,A) ex y being Element of ND (V,A) st S1[n,x,y]
let x be
Element of
ND (
V,
A);
ex y being Element of ND (V,A) st S1[n,x,y]
set y =
local_overlapping (
V,
A,
x,
((prg . (n + 1)) . x),
(loc /. (pos . (n + 1))));
local_overlapping (
V,
A,
x,
((prg . (n + 1)) . x),
(loc /. (pos . (n + 1))))
in ND (
V,
A)
;
then reconsider y =
local_overlapping (
V,
A,
x,
((prg . (n + 1)) . x),
(loc /. (pos . (n + 1)))) as
Element of
ND (
V,
A) ;
take
y
;
S1[n,x,y]
thus
S1[
n,
x,
y]
;
verum
end;
local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) in ND (V,A)
;
then reconsider X = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) as Element of ND (V,A) ;
ex p being FinSequence of ND (V,A) st
( len p = len prg & ( p . 1 = X or len prg = 0 ) & ( for n being Nat st 1 <= n & n < len prg holds
S1[n,p . n,p . (n + 1)] ) )
from RECDEF_1:sch 4(A2);
hence
ex b1 being FinSequence of ND (V,A) st
( len b1 = len prg & b1 . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len b1 holds
b1 . (n + 1) = local_overlapping (V,A,(b1 . n),((prg . (n + 1)) . (b1 . n)),(loc /. (pos . (n + 1)))) ) )
by A1; verum