deffunc H1( 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 = H1(d)
from FUNCT_2:sch 4();
take
f
; for w being Element of Omega holds f . w = PortfolioValueFut ((d + 1),phi,F,G,w)
let n be Element of Omega; f . n = PortfolioValueFut ((d + 1),phi,F,G,n)
thus
f . n = PortfolioValueFut ((d + 1),phi,F,G,n)
by A1; verum