deffunc H₁( Nat) -> set = (f . $1) |^ a;
consider p being FinSequence such that
A1: ( len p = len f & ( 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 & ( for i being set st i in dom p holds
p . i = (f . i) |^ a ) ) by A1; :: thesis: verum