let F1, F2 be FinSequence of PFuncs ((ND (V,A)),(ND (V,A))); :: thesis: ( len F1 = size & F1 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds
F1 . (n + 1) = PP_composition ((F1 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) & len F2 = size & F2 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds
F2 . (n + 1) = PP_composition ((F2 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) implies F1 = F2 )
assume that
A6: len F1 = size and
A7: F1 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) and
A8: for n being Nat st 1 <= n & n < size holds
F1 . (n + 1) = PP_composition ((F1 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) and
A9: len F2 = size and
A10: F2 . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) and
A11: for n being Nat st 1 <= n & n < size holds
F2 . (n + 1) = PP_composition ((F2 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ; :: thesis: F1 = F2
A12: for n being Nat st 1 <= n & n < size holds
for x, y1, y2 being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
A13: ( len F1 = size & ( F1 . 1 = X or size = 0 ) & ( for n being Nat st 1 <= n & n < size holds
S₁[n,F1 . n,F1 . (n + 1)] ) )

proof

thus len F1 = size by A6; :: thesis: ( ( F1 . 1 = X or size = 0 ) & ( for n being Nat st 1 <= n & n < size holds
S₁[n,F1 . n,F1 . (n + 1)] ) )
thus ( F1 . 1 = X or size = 0 ) by A7; :: thesis: for n being Nat st 1 <= n & n < size holds
S₁[n,F1 . n,F1 . (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < size implies S₁[n,F1 . n,F1 . (n + 1)] )
assume ( 1 <= n & n < size ) ; :: thesis: S₁[n,F1 . n,F1 . (n + 1)]
then F1 . (n + 1) = PP_composition ((F1 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) by A8;
hence S₁[n,F1 . n,F1 . (n + 1)] ; :: thesis: verum

end;

A14: ( len F2 = size & ( F2 . 1 = X or size = 0 ) & ( for n being Nat st 1 <= n & n < size holds
S₁[n,F2 . n,F2 . (n + 1)] ) )

proof

thus len F2 = size by A9; :: thesis: ( ( F2 . 1 = X or size = 0 ) & ( for n being Nat st 1 <= n & n < size holds
S₁[n,F2 . n,F2 . (n + 1)] ) )
thus ( F2 . 1 = X or size = 0 ) by A10; :: thesis: for n being Nat st 1 <= n & n < size holds
S₁[n,F2 . n,F2 . (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < size implies S₁[n,F2 . n,F2 . (n + 1)] )
assume ( 1 <= n & n < size ) ; :: thesis: S₁[n,F2 . n,F2 . (n + 1)]
then F2 . (n + 1) = PP_composition ((F2 . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) by A11;
hence S₁[n,F2 . n,F2 . (n + 1)] ; :: thesis: verum

end;

thus F1 = F2 from RECDEF_1:sch 8(A12, A13, A14); :: thesis: verum