theorem :: MATRTOP1:1

for rf1, rf2 being real-valued FinSequence holds (@ rf1) + (@ rf2) = rf1 + rf2 by RVSUM_1:def 4;