:: deftheorem defines FinS2MX MATRIX13:def 5 :
for K being Field
for n being Nat
for F being FinSequence of (n -VectSp_over K) holds FinS2MX F = F;