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

proof

let n be Nat; :: thesis: ( 1 <= n & n < len val implies for x being Element of PFuncs ((ND (V,A)),BOOLEAN) ex y being Element of PFuncs ((ND (V,A)),BOOLEAN) st S₁[n,x,y] )
assume ( 1 <= n & n < len val ) ; :: thesis: for x being Element of PFuncs ((ND (V,A)),BOOLEAN) ex y being Element of PFuncs ((ND (V,A)),BOOLEAN) st S₁[n,x,y]
let x be Element of PFuncs ((ND (V,A)),BOOLEAN); :: thesis: ex y being Element of PFuncs ((ND (V,A)),BOOLEAN) st S₁[n,x,y]
reconsider f = x as SCPartialNominativePredicate of V,A by PARTFUN1:47;
set y = SC_Psuperpos (f,(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n)));
reconsider y = SC_Psuperpos (f,(denaming (V,A,(val . ((len val) - n)))),(loc /. ((len val) - n))) as Element of PFuncs ((ND (V,A)),BOOLEAN) by PARTFUN1:45;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

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