:: deftheorem defines Base_FinSeq MATRIXR2:def 4 :
for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1);