A2: for n being Nat st 1 <= n & n < size 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 < size 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 < size ) ; :: 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,((denaming (V,A,(val . (n + 1)))) . x),(loc /. (n + 1)));
local_overlapping (V,A,x,((denaming (V,A,(val . (n + 1)))) . x),(loc /. (n + 1))) in ND (V,A) ;
then reconsider y = local_overlapping (V,A,x,((denaming (V,A,(val . (n + 1)))) . x),(loc /. (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,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) in ND (V,A) ;
then reconsider X = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) as Element of ND (V,A) ;
ex p being FinSequence of ND (V,A) st
( len p = size & ( p . 1 = X or size = 0 ) & ( for n being Nat st 1 <= n & n < size 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₁ = size & b₁ . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len b₁ holds
b₁ . (n + 1) = local_overlapping (V,A,(b₁ . n),((denaming (V,A,(val . (n + 1)))) . (b₁ . n)),(loc /. (n + 1))) ) ) by A1; :: thesis: verum