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 S₁[n,x,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < len prg implies for x being Element of ND (V,A) ex y being Element of ND (V,A) st S₁[n,x,y] )
assume ( 1 <= n & n < len prg ) ; :: thesis: for x being Element of ND (V,A) ex y being Element of ND (V,A) st S₁[n,x,y]
let x be Element of ND (V,A); :: thesis: ex y being Element of ND (V,A) st S₁[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 ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: 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
S₁[n,p . n,p . (n + 1)] ) ) from RECDEF_1:sch 4(A2);
hence ex b₁ being FinSequence of ND (V,A) st
( len b₁ = len prg & b₁ . 1 = local_overlapping (V,A,d1,((prg . 1) . d1),(loc /. (pos . 1))) & ( for n being Nat st 1 <= n & n < len b₁ holds
b₁ . (n + 1) = local_overlapping (V,A,(b₁ . n),((prg . (n + 1)) . (b₁ . n)),(loc /. (pos . (n + 1)))) ) ) by A1; :: thesis: verum