:: deftheorem defines @ MATRTOP1:def 2 :
for p being FinSequence of F_Real holds @ p = p;