deffunc H₁( Nat) -> Element of NAT = In ((primenumber ($1 -' 1)),NAT);
consider f being FinSequence of NAT such that
A1: len f = k and
A2: for j being Nat st j in dom f holds
f . j = H₁(j) from FINSEQ_2:sch 1();
take f ; :: thesis: ( len f = k & ( for i being Nat st i < k holds
f . (i + 1) = primenumber i ) )
thus len f = k by A1; :: thesis: for i being Nat st i < k holds
f . (i + 1) = primenumber i
let i be Nat; :: thesis: ( i < k implies f . (i + 1) = primenumber i )
assume i < k ; :: thesis: f . (i + 1) = primenumber i
then ( 0 + 1 <= i + 1 & i + 1 <= k ) by NAT_1:13;
hence f . (i + 1) = H₁(i + 1) by A1, A2, FINSEQ_3:25
.= primenumber i ;
:: thesis: verum