A2: for n being Nat st 1 <= n & n < len fD holds
for x being Element of PFuncs (D,D) ex y being Element of PFuncs (D,D) st S₁[n,x,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < len fD implies for x being Element of PFuncs (D,D) ex y being Element of PFuncs (D,D) st S₁[n,x,y] )
assume ( 1 <= n & n < len fD ) ; :: thesis: for x being Element of PFuncs (D,D) ex y being Element of PFuncs (D,D) st S₁[n,x,y]
let x be Element of PFuncs (D,D); :: thesis: ex y being Element of PFuncs (D,D) st S₁[n,x,y]
reconsider g = x as PartFunc of D,D by PARTFUN1:46;
reconsider y = PP_composition (g,(fD . (n + 1))) as Element of PFuncs (D,D) by PARTFUN1:45;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

consider F being FinSequence of PFuncs (D,D) such that
A3: len F = len fD and
A4: ( F . 1 = X or len fD = 0 ) and
A5: for n being Nat st 1 <= n & n < len fD holds
S₁[n,F . n,F . (n + 1)] from RECDEF_1:sch 4(A2);
take F ; :: thesis: ( len F = len fD & F . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds
F . (n + 1) = PP_composition ((F . n),(fD . (n + 1))) ) )
thus len F = len fD by A3; :: thesis: ( F . 1 = fD . 1 & ( for n being Nat st 1 <= n & n < len fD holds
F . (n + 1) = PP_composition ((F . n),(fD . (n + 1))) ) )
thus F . 1 = fD . 1 by A1, A4; :: thesis: for n being Nat st 1 <= n & n < len fD holds
F . (n + 1) = PP_composition ((F . n),(fD . (n + 1)))
let n be Nat; :: thesis: ( 1 <= n & n < len fD implies F . (n + 1) = PP_composition ((F . n),(fD . (n + 1))) )
assume ( 1 <= n & n < len fD ) ; :: thesis: F . (n + 1) = PP_composition ((F . n),(fD . (n + 1)))
then S₁[n,F . n,F . (n + 1)] by A5;
hence F . (n + 1) = PP_composition ((F . n),(fD . (n + 1))) ; :: thesis: verum