reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Nat) -> Element of REAL = In (($1 |^ n),REAL);
consider e being FinSequence of REAL such that
A1: ( len e = k1 & ( for i being Nat st i in dom e holds
e . i = H₁(i) ) ) from FINSEQ_2:sch 1();
take e ; :: thesis: ( dom e = Seg k & ( for i being Nat st i in dom e holds
e . i = i |^ n ) )
thus dom e = Seg k by FINSEQ_1:def 3, A1; :: thesis: for i being Nat st i in dom e holds
e . i = i |^ n
let i be Nat; :: thesis: ( i in dom e implies e . i = i |^ n )
assume A2: i in dom e ; :: thesis: e . i = i |^ n
H₁(i) = i |^ n ;
hence e . i = i |^ n by A2, A1; :: thesis: verum