let F1, F2 be FinSequence of PFuncs ((ND (V,A)),BOOLEAN); :: thesis: ( len F1 = len val & F1 . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) & ( for n being Nat st 1 <= n & n < len F1 holds
F1 . (n + 1) = SC_Psuperpos ((F1 . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) & len F2 = len val & F2 . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) & ( for n being Nat st 1 <= n & n < len F2 holds
F2 . (n + 1) = SC_Psuperpos ((F2 . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ) implies F1 = F2 )
assume that
A5: len F1 = len val and
A6: F1 . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) and
A7: for n being Nat st 1 <= n & n < len F1 holds
F1 . (n + 1) = SC_Psuperpos ((F1 . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) and
A8: len F2 = len val and
A9: F2 . 1 = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) and
A10: for n being Nat st 1 <= n & n < len F2 holds
F2 . (n + 1) = SC_Psuperpos ((F2 . n),(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) ; :: thesis: F1 = F2
reconsider X = SC_Psuperpos (p,(denaming (V,A,(val . (len val)))),(loc /. (len val))) as Element of PFuncs ((ND (V,A)),BOOLEAN) by PARTFUN1:45;
A11: for n being Nat st 1 <= n & n < len val holds
for x, y1, y2 being Element of PFuncs ((ND (V,A)),BOOLEAN) st S₁[n,x,y1] & S₁[n,x,y2] holds
y1 = y2 ;
A12: ( len F1 = len val & ( F1 . 1 = X or len val = 0 ) & ( for n being Nat st 1 <= n & n < len val holds
S₁[n,F1 . n,F1 . (n + 1)] ) )

proof

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

end;

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

proof

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

end;

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