let n be Nat; :: thesis: for F being FinSequence of (REAL-NS n)
for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
let F be FinSequence of (REAL-NS n); :: thesis: for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds
Sum F = Sum Fv
let Fv be FinSequence of (n -VectSp_over F_Real); :: thesis: ( Fv = F implies Sum F = Sum Fv )
assume A1: Fv = F ; :: thesis: Sum F = Sum Fv
reconsider Ft = F as FinSequence of (TOP-REAL n) by Th4;
Sum F = Sum Ft by Th21;
hence Sum F = Sum Fv by A1, MATRTOP2:4; :: thesis: verum