deffunc H₁( Element of NAT ) -> Element of REAL = (RVElementsOfPortfolioValue_fut (phi,F,G,$1)) . w;
consider f being Real_Sequence such that
A1: for d being Element of NAT holds f . d = H₁(d) from FUNCT_2:sch 4();
take f ; :: thesis: for n being Nat holds f . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
let n be Nat; :: thesis: f . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
reconsider n = n as Element of NAT by ORDINAL1:def 12;
f . n = H₁(n) by A1;
hence f . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ; :: thesis: verum