A2: for n being Nat st 1 <= n & n < size holds
for x being Element of PFuncs ((ND (V,A)),(ND (V,A))) ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < size implies for x being Element of PFuncs ((ND (V,A)),(ND (V,A))) ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x,y] )
assume ( 1 <= n & n < size ) ; :: thesis: for x being Element of PFuncs ((ND (V,A)),(ND (V,A))) ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x,y]
let x be Element of PFuncs ((ND (V,A)),(ND (V,A))); :: thesis: ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x,y]
reconsider f = x as PartFunc of (ND (V,A)),(ND (V,A)) by PARTFUN1:46;
reconsider y = PP_composition (f,(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) as Element of PFuncs ((ND (V,A)),(ND (V,A))) by PARTFUN1:45;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

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