deffunc H₁( Element of Omega) -> Element of REAL = PortfolioValueFutExt (d,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 = PortfolioValueFutExt (d,phi,F,G,w)
let n be Element of Omega; :: thesis: f . n = PortfolioValueFutExt (d,phi,F,G,n)
thus f . n = PortfolioValueFutExt (d,phi,F,G,n) by A1; :: thesis: verum