defpred S₁[ Nat, set ] means $2 = (f /. $1) `2 ;
A12: 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
A13: dom v = Seg (len f) and
A14: for k being Nat st k in Seg (len f) holds
S<sub>1</sub>[k,v . k] from FINSEQ_1:sch 5(A12);
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 A13, 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 A13, A14; :: thesis: verum