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 that
A1: len x = n and
A2: len y = n and
A3: x * A = y ; :: thesis: for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col A,j))|
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 A2, A3;
hence y . j = |(x,(Col A,j))| by A1, A3, MATRIX_1:25, MATRPROB:40; :: thesis: verum