defpred S₁[ Nat, set ] means for G being Element of PFuncs D,REAL st f . $1 = G holds
$2 = G . 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:13;
take x = G . d; :: thesis: S₁[n,x]
thus S₁[n,x] ; :: 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
for G being Element of PFuncs D,REAL st n in dom p & f . n = G holds
p . n = G . d ) )
thus len p = len f by A2, FINSEQ_1:def 3; :: thesis: for n being Element of NAT
for G being Element of PFuncs D,REAL st n in dom p & f . n = G holds
p . n = G . d
let n be Element of NAT ; :: thesis: for G being Element of PFuncs D,REAL st n in dom p & f . n = G holds
p . n = G . d
let G be Element of PFuncs D,REAL ; :: thesis: ( n in dom p & f . n = G implies p . n = G . d )
assume ( n in dom p & f . n = G ) ; :: thesis: p . n = G . d
hence p . n = G . d by A2, A3; :: thesis: verum