let F, G be FinSequence of ND (V,A); :: thesis: ( len F = size & F . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len F holds
F . (n + 1) = local_overlapping (V,A,(F . n),((denaming (V,A,(val . (n + 1)))) . (F . n)),(loc /. (n + 1))) ) & len G = size & G . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) & ( for n being Nat st 1 <= n & n < len G holds
G . (n + 1) = local_overlapping (V,A,(G . n),((denaming (V,A,(val . (n + 1)))) . (G . n)),(loc /. (n + 1))) ) implies F = G )
assume that
A3: len F = size and
A4: F . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) and
A5: for n being Nat st 1 <= n & n < len F holds
F . (n + 1) = local_overlapping (V,A,(F . n),((denaming (V,A,(val . (n + 1)))) . (F . n)),(loc /. (n + 1))) and
A6: len G = size and
A7: G . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) and
A8: for n being Nat st 1 <= n & n < len G holds
G . (n + 1) = local_overlapping (V,A,(G . n),((denaming (V,A,(val . (n + 1)))) . (G . n)),(loc /. (n + 1))) ; :: thesis: F = G
A9: for n being Nat st 1 <= n & n < size holds
for x, y1, y2 being set st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
A10: ( len F = size & ( F . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) or size = 0 ) & ( for n being Nat st 1 <= n & n < size holds
S₁[n,F . n,F . (n + 1)] ) ) by A3, A4, A5;
A11: ( len G = size & ( G . 1 = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) or size = 0 ) & ( for n being Nat st 1 <= n & n < size holds
S₁[n,G . n,G . (n + 1)] ) ) by A6, A7, A8;
thus F = G from RECDEF_1:sch 7(A9, A10, A11); :: thesis: verum