deffunc H₁( Element of Omega) -> Element of REAL = PortfolioValueFut ((d + 1),phi,F,G,$1);
consider f being Function of Omega,REAL such that
A1: for d being Element of Omega holds f . d = H₁(d) from FUNCT_2:sch 4();
take f ; :: thesis: for w being Element of Omega holds f . w = PortfolioValueFut ((d + 1),phi,F,G,w)
let n be Element of Omega; :: thesis: f . n = PortfolioValueFut ((d + 1),phi,F,G,n)
thus f . n = PortfolioValueFut ((d + 1),phi,F,G,n) by A1; :: thesis: verum