let rf1, rf2 be real-valued FinSequence; :: thesis: (@ rf1) + (@ rf2) = rf1 + rf2
thus (@ rf1) + (@ rf2) = the addF of F_Real .: (rf1,rf2) by FVSUM_1:def 3
.= rf1 + rf2 by RVSUM_1:def 4 ; :: thesis: verum