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

proof

let k be Nat; :: thesis: ( k in Seg (len f) implies ex r being Element of REAL st S₁[k,r] )
(f /. k) `1 in REAL by XREAL_0:def 1;
hence ( k in Seg (len f) implies ex r being Element of REAL st S₁[k,r] ) ; :: thesis: verum

end;

consider v being FinSequence of REAL such that
A2: dom v = Seg (len f) and
A3: for k being Nat st k in Seg (len f) holds
S₁[k,v . k] from FINSEQ_1:sch 5(A1);
take v ; :: thesis: ( len v = len f & ( for n being Nat st n in dom v holds
v . n = (f /. n) `1 ) )
thus len v = len f by A2, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom v holds
v . n = (f /. n) `1
let n be Nat; :: thesis: ( n in dom v implies v . n = (f /. n) `1 )
assume n in dom v ; :: thesis: v . n = (f /. n) `1
hence v . n = (f /. n) `1 by A2, A3; :: thesis: verum