defpred S₁[ Nat, set ] means $2 = (f /. $1) `1 ;
A1: 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
A2: dom v = Seg (len f) and
A3: for k being Nat st k in Seg (len f) holds
S<sub>1</sub>[k,v . k] from FINSEQ_1:sch 5(A1);
take v ; :: thesis: ( len v = len f & ( for n being Element of 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 Element of NAT st n in dom v holds
v . n = (f /. n) `1
let n be Element of 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