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

proof

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

end;

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

proof

thus len F2 = len fD by A9; :: thesis: ( ( F2 . 1 = X or len fD = 0 ) & ( for n being Nat st 1 <= n & n < len fD holds
S₁[n,F2 . n,F2 . (n + 1)] ) )
thus ( F2 . 1 = X or len fD = 0 ) by A10; :: thesis: for n being Nat st 1 <= n & n < len fD holds
S₁[n,F2 . n,F2 . (n + 1)]
let n be Nat; :: thesis: ( 1 <= n & n < len fD implies S₁[n,F2 . n,F2 . (n + 1)] )
assume ( 1 <= n & n < len fD ) ; :: thesis: S₁[n,F2 . n,F2 . (n + 1)]
then F2 . (n + 1) = PP_composition ((F2 . n),(fD . (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