defpred S₁[ Nat, set ] means $2 = (f /. $1) `2 ;
A12: 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) `2 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
A13: dom v = Seg (len f) and
A14: for k being Nat st k in Seg (len f) holds
S₁[k,v . k] from FINSEQ_1:sch 5(A12);
take v ; :: thesis: ( len v = len f & ( for n being Nat st n in dom v holds
v . n = (f /. n) `2 ) )
thus len v = len f by A13, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom v holds
v . n = (f /. n) `2
let n be Nat; :: thesis: ( n in dom v implies v . n = (f /. n) `2 )
assume n in dom v ; :: thesis: v . n = (f /. n) `2
hence v . n = (f /. n) `2 by A13, A14; :: thesis: verum