deffunc H₁( Nat) -> Element of REAL = In (((b + $1) to_power e),REAL);
consider f being FinSequence of REAL such that
A1: len f = n 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 = n & ( for i being Nat st 1 <= i & i <= n holds
f . i = (b + i) to_power e ) )
thus len f = n by A1; :: thesis: for i being Nat st 1 <= i & i <= n holds
f . i = (b + i) to_power e
let i be Nat; :: thesis: ( 1 <= i & i <= n implies f . i = (b + i) to_power e )
assume ( 1 <= i & i <= n ) ; :: thesis: f . i = (b + i) to_power e
then i in dom f by A1, FINSEQ_3:25;
then f . i = H₁(i) by A2;
hence f . i = (b + i) to_power e ; :: thesis: verum