theorem Th31: :: BKMODEL1:35

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)