deffunc H₁( Element of NAT ) -> Element of REAL = Sum (Prob * (@Shift_Seq (A,$1)));
consider f being Real_Sequence such that
A1: for k being Element of NAT holds f . k = H₁(k) from FUNCT_2:sch 4();
take f ; :: thesis: for n being Element of NAT holds f . n = Sum (Prob * (@Shift_Seq (A,n)))
let knat be Nat; :: thesis: ( knat is Element of REAL & knat is Element of NAT implies f . knat = Sum (Prob * (@Shift_Seq (A,knat))) )
thus ( knat is Element of REAL & knat is Element of NAT implies f . knat = Sum (Prob * (@Shift_Seq (A,knat))) ) by A1; :: thesis: verum