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 S1[n,x,y1] & S1[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
S1[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
S1[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
S1[n,F1 . n,F1 . (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < size implies S1[n,F1 . n,F1 . (n + 1)] )
assume ( 1 <= n & n < size ) ; :: thesis: S1[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 S1[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
S1[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
S1[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
S1[n,F2 . n,F2 . (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < size implies S1[n,F2 . n,F2 . (n + 1)] )
assume ( 1 <= n & n < size ) ; :: thesis: S1[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 S1[n,F2 . n,F2 . (n + 1)] ; :: thesis: verum
end;
thus F1 = F2 from RECDEF_1:sch 8(A12, A13, A14); :: thesis: verum