A1: for n being Nat st n in Seg (len val) holds
ex x being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x]

proof

let n be Nat; :: thesis: ( n in Seg (len val) implies ex x being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x] )
assume n in Seg (len val) ; :: thesis: ex x being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S₁[n,x]
reconsider x = denaming (V,A,(val . n)) as Element of PFuncs ((ND (V,A)),(ND (V,A))) by PARTFUN1:45;
take x ; :: thesis: S₁[n,x]
thus S₁[n,x] ; :: thesis: verum

end;

consider p being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) such that
A2: dom p = Seg (len val) and
A3: for n being Nat st n in Seg (len val) holds
S₁[n,p . n] from FINSEQ_1:sch 5(A1);
take p ; :: thesis: ( len p = len val & ( for n being Nat st 1 <= n & n <= len p holds
p . n = denaming (V,A,(val . n)) ) )
thus len p = len val by A2, FINSEQ_1:def 3; :: thesis: for n being Nat st 1 <= n & n <= len p holds
p . n = denaming (V,A,(val . n))
thus for n being Nat st 1 <= n & n <= len p holds
p . n = denaming (V,A,(val . n)) by A2, A3, FINSEQ_3:25; :: thesis: verum