for N being Matrix of 3,REAL
for uf being FinSequence of REAL st uf = 0. (TOP-REAL 3) holds
N * uf = 0. (TOP-REAL 3)