theorem Th18: :: MATRTOP2:18

for n, m being Nat
for M being Matrix of n,m,F_Real holds rng (Mx2Tran M) = [#] (Lin (lines M))