let f1, f2 be Function of Omega,REAL; :: thesis: ( ( 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) ; :: thesis: f1 = f2
for w being Element of Omega holds f1 . w = f2 . w

proof

let w be Element of Omega; :: thesis: f1 . w = f2 . w
f2 . w = PortfolioValueFut ((d + 1),phi,F,G,w) by A3;
hence f1 . w = f2 . w by A2; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum