let n be 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 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 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 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 Nat st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|
let j be 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_0:24, MATRPROB:40; :: thesis: verum