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