:: deftheorem defines + RVSUM_1:def 4 :
for F1, F2 being real-valued FinSequence holds F1 + F2 = addreal .: (F1,F2);