deffunc H₁( Nat) -> Element of ExtREAL = Sum (e . $1);
consider e1 being FinSequence of ExtREAL 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 & ( for k being Nat st k in dom e1 holds
e1 . k = Sum (e . k) ) ) by A1; :: thesis: verum