defpred S_{1}[ 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_{1}[k,r]

A13: dom v = Seg (len f) and

A14: for k being Nat st k in Seg (len f) holds

S_{1}[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

A12: for k being Nat st k in Seg (len f) holds

ex r being Element of REAL st S

proof

consider v being FinSequence of REAL such that
let k be Nat; :: thesis: ( k in Seg (len f) implies ex r being Element of REAL st S_{1}[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_{1}[k,r] )
; :: thesis: verum

end;(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

A13: dom v = Seg (len f) and

A14: for k being Nat st k in Seg (len f) holds

S

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