for N being invertible Matrix of 3,F_Real
for u, mu being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for ut being FinSequence of 1 -tuples_on REAL st not u is zero & u = uf & ut = N * uf & mu = M2F ut holds
not mu is zero