let f1, f2 be Function of Omega,REAL; ( ( for w being Element of Omega holds f1 . w = PortfolioValueFut ((d + 1),phi,F,G,w) ) & ( for w being Element of Omega holds f2 . w = PortfolioValueFut ((d + 1),phi,F,G,w) ) implies f1 = f2 )
assume that
A2:
for w being Element of Omega holds f1 . w = PortfolioValueFut ((d + 1),phi,F,G,w)
and
A3:
for w being Element of Omega holds f2 . w = PortfolioValueFut ((d + 1),phi,F,G,w)
; f1 = f2
for w being Element of Omega holds f1 . w = f2 . w
hence
f1 = f2
; verum