let f1, f2 be Function of Omega,REAL; :: thesis: ( ( for w being Element of Omega holds f1 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for w being Element of Omega holds f2 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) implies f1 = f2 )
assume that
A2: for w being Element of Omega holds f1 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) and
A3: for w being Element of Omega holds f2 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ; :: 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 = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) by A3;
hence f1 . w = f2 . w by A2; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum