theorem Th30: :: MATRIX11:30

for l, n, m being Nat
for D being non empty set
for M being Matrix of n,m,D holds M = RLine (M,l,(Line (M,l)))