:: deftheorem defines @ MATRTOP1:def 1 :
for rf being real-valued FinSequence holds @ rf = rf;