theorem Th88: :: MATRIXR2:88

for n being Nat
for x being FinSequence of REAL st len x = n holds
x * (1_Rmatrix n) = x