let f1, f2 be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds f1 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for n being Element of NAT holds f2 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) implies f1 = f2 )
assume that
A2: for d being Element of NAT holds f1 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) and
A3: for d being Element of NAT holds f2 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) ; :: thesis: f1 = f2
let d be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: f1 . d = f2 . d
( f1 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) & f2 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) ) by A2, A3;
hence f1 . d = f2 . d ; :: thesis: verum