defpred S₁[ Nat, set ] means $2 = (f /. $1) `2 ;
A8: for k being Nat st k in Seg (len f) holds
ex r being Real st S<sub>1</sub>[k,r] ;
consider v being FinSequence of REAL such that
A9: dom v = Seg (len f) and
A10: for k being Nat st k in Seg (len f) holds
S<sub>1</sub>[k,v . k] from FINSEQ_1:sch 5(A8);
take v ; :: thesis: ( len v = len f & ( for n being Element of NAT st n in dom v holds
v . n = (f /. n) `2 ) )
thus len v = len f by A9, FINSEQ_1:def 3; :: thesis: for n being Element of NAT st n in dom v holds
v . n = (f /. n) `2
let n be Element of 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 A9, A10; :: thesis: verum