defpred S₁[ Nat, set ] means $2 = (f . $1) . d;
A1: for n being Nat st n in Seg (len f) holds
ex x being Element of REAL st S₁[n,x]

proof

let n be Nat; :: thesis: ( n in Seg (len f) implies ex x being Element of REAL st S₁[n,x] )
assume n in Seg (len f) ; :: thesis: ex x being Element of REAL st S₁[n,x]
then n in dom f by FINSEQ_1:def 3;
then reconsider G = f . n as Element of PFuncs (D,REAL) by FINSEQ_2:11;
take G . d ; :: thesis: ( G . d is Element of REAL & S₁[n,G . d] )
thus ( G . d is Element of REAL & S₁[n,G . d] ) by XREAL_0:def 1; :: thesis: verum

end;

consider p being FinSequence of REAL such that
A2: dom p = Seg (len f) and
A3: for n being Nat st n in Seg (len f) holds
S₁[n,p . n] from FINSEQ_1:sch 5(A1);
take p ; :: thesis: ( len p = len f & ( for n being Element of NAT st n in dom p holds
p . n = (f . n) . d ) )
thus len p = len f by A2, FINSEQ_1:def 3; :: thesis: for n being Element of NAT st n in dom p holds
p . n = (f . n) . d
thus for n being Element of NAT st n in dom p holds
p . n = (f . n) . d by A2, A3; :: thesis: verum