theorem :: REAL_NS2:75

for T being RealLinearSpace
for Ft being FinSequence of T
for Fr being FinSequence of (RLSp2RVSp T) st Ft = Fr holds
Sum Ft = Sum Fr ;