let n be Nat; :: thesis: dom (1_Rmatrix n) = Seg n
len (1_Rmatrix n) = n by MATRIX_0:24;
hence dom (1_Rmatrix n) = Seg n by FINSEQ_1:def 3; :: thesis: verum