deffunc H₁( Nat) -> Element of REAL = In ((Sum (e . $1)),REAL);
consider e1 being FinSequence of REAL such that
A1: ( len e1 = len e & ( for k being Nat st k in dom e1 holds
e1 . k = H₁(k) ) ) from FINSEQ_2:sch 1();
take e1 ; :: thesis: ( len e1 = len e & ( for k being Nat st k in dom e1 holds
e1 . k = Sum (e . k) ) )
thus len e1 = len e by A1; :: thesis: for k being Nat st k in dom e1 holds
e1 . k = Sum (e . k)
let k be Nat; :: thesis: ( k in dom e1 implies e1 . k = Sum (e . k) )
assume k in dom e1 ; :: thesis: e1 . k = Sum (e . k)
then e1 . k = H₁(k) by A1;
hence e1 . k = Sum (e . k) ; :: thesis: verum