deffunc H_{1}( Nat) -> Element of REAL = In ((Sum (Prob * (A ^\ $1))),REAL);

consider f being Real_Sequence such that

A1: for k being Element of NAT holds f . k = H_{1}(k)
from FUNCT_2:sch 4();

take f ; :: thesis: for n being Nat holds f . n = Sum (Prob * (A ^\ n))

let k be Nat; :: thesis: f . k = Sum (Prob * (A ^\ k))

k in NAT by ORDINAL1:def 12;

then f . k = H_{1}(k)
by A1;

hence f . k = Sum (Prob * (A ^\ k)) ; :: thesis: verum

consider f being Real_Sequence such that

A1: for k being Element of NAT holds f . k = H

take f ; :: thesis: for n being Nat holds f . n = Sum (Prob * (A ^\ n))

let k be Nat; :: thesis: f . k = Sum (Prob * (A ^\ k))

k in NAT by ORDINAL1:def 12;

then f . k = H

hence f . k = Sum (Prob * (A ^\ k)) ; :: thesis: verum