for n being Nat
for A being Matrix of n,REAL
for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds
for j being Nat st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|