theorem Th13: :: ANPROJ_8:15

for n being Nat holds dom (1_Rmatrix n) = Seg n