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