let n be Element of NAT ; :: thesis: 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 Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col A,j))|
let A be Matrix of n, REAL ; :: thesis: for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds
for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col A,j))|
let x, y be FinSequence of REAL ; :: thesis: ( len x = n & len y = n & x * A = y implies for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col A,j))| )
assume A1: ( len x = n & len y = n & x * A = y ) ; :: thesis: for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col A,j))|
A2: ( len A = n & width A = n ) by MATRIX_1:25;
let j be Element of NAT ; :: thesis: ( 1 <= j & j <= n implies y . j = |(x,(Col A,j))| )
assume ( 1 <= j & j <= n ) ; :: thesis: y . j = |(x,(Col A,j))|
then j in Seg (len (x * A)) by A1;
hence y . j = |(x,(Col A,j))| by A1, A2, MATRPROB:40; :: thesis: verum