deffunc H₁( Nat) -> Element of REAL = (f . $1) |^ a;
consider p being FinSequence such that
A1: len p = len f and
A2: for k being Nat st k in dom p holds
p . k = H₁(k) from FINSEQ_1:sch 2();
take p ; :: thesis: ( len p = len f & ( for i being set st i in dom p holds
p . i = (f . i) |^ a ) )
thus len p = len f by A1; :: thesis: for i being set st i in dom p holds
p . i = (f . i) |^ a
let i be set ; :: thesis: ( i in dom p implies p . i = (f . i) |^ a )
assume i in dom p ; :: thesis: p . i = (f . i) |^ a
hence p . i = (f . i) |^ a by A2; :: thesis: verum