for i, n being Nat st 1 <= i & i <= n holds
(1_Rmatrix n) . i = Base_FinSeq (n,i)