let f1, f2 be Real_Sequence; :: thesis: ( ( for n being Nat holds f1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) & ( for n being Nat holds f2 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) implies f1 = f2 )
assume that
A1: for n being Nat holds f1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w and
A2: for n being Nat holds f2 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ; :: thesis: f1 = f2
for n being Nat holds f1 . n = f2 . n

proof

let n be Nat; :: thesis: f1 . n = f2 . n
f1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w by A1;
hence f1 . n = f2 . n by A2; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum