:: deftheorem defines Base_FinSeq MATRIX14:def 2 :
for K being Field
for n, i being Nat holds Base_FinSeq (K,n,i) = Replace ((n |-> (0. K)),i,(1. K));